:: LATSUBGR semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: LATSUBGR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G holds the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2
proof end;

theorem Th2: :: LATSUBGR:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for h being set holds
( h in Subgroups G iff ex H being strict Subgroup of G st h = H )
proof end;

theorem Th3: :: LATSUBGR:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G
for H being strict Subgroup of G st A = the carrier of H holds
gr A = H
proof end;

theorem Th4: :: LATSUBGR:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds
H1 "\/" H2 = gr A
proof end;

theorem Th5: :: LATSUBGR:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for g being Element of G st ( g in H1 or g in H2 ) holds
g in H1 "\/" H2
proof end;

theorem :: LATSUBGR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2
for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1
proof end;

theorem :: LATSUBGR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2
for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2
proof end;

theorem :: LATSUBGR:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATSUBGR:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATSUBGR:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2
for H1, H2 being Subgroup of G1
for H3, H4 being Subgroup of G2 st the carrier of H3 = f .: the carrier of H1 & the carrier of H4 = f .: the carrier of H2 & H1 is Subgroup of H2 holds
H3 is Subgroup of H4
proof end;

theorem :: LATSUBGR:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2
for H1, H2 being Subgroup of G2
for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds
H3 is Subgroup of H4
proof end;

theorem :: LATSUBGR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Function of the carrier of G1,the carrier of G2
for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)
proof end;

theorem :: LATSUBGR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for H1, H2 being Subgroup of G1
for f being Function of the carrier of G1,the carrier of G2
for A being Subset of G1 st A = the carrier of H1 \/ the carrier of H2 holds
f .: the carrier of (H1 "\/" H2) = f .: the carrier of (gr A) by Th4;

theorem Th14: :: LATSUBGR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for A being Subset of G st A = {(1. G)} holds
gr A = (1). G
proof end;

definition
let G be Group;
func carr G -> Function of Subgroups G, bool the carrier of G means :Def1: :: LATSUBGR:def 1
for H being strict Subgroup of G holds it . H = the carrier of H;
existence
ex b1 being Function of Subgroups G, bool the carrier of G st
for H being strict Subgroup of G holds b1 . H = the carrier of H
proof end;
uniqueness
for b1, b2 being Function of Subgroups G, bool the carrier of G st ( for H being strict Subgroup of G holds b1 . H = the carrier of H ) & ( for H being strict Subgroup of G holds b2 . H = the carrier of H ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines carr LATSUBGR:def 1 :
for G being Group
for b2 being Function of Subgroups G, bool the carrier of G holds
( b2 = carr G iff for H being strict Subgroup of G holds b2 . H = the carrier of H );

theorem :: LATSUBGR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATSUBGR:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATSUBGR:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th18: :: LATSUBGR:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G
for x being Element of G holds
( x in (carr G) . H iff x in H )
proof end;

theorem :: LATSUBGR:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G holds 1. G in (carr G) . H
proof end;

theorem :: LATSUBGR:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G holds (carr G) . H <> {}
proof end;

theorem :: LATSUBGR:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G
for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds
g1 * g2 in (carr G) . H
proof end;

theorem :: LATSUBGR:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H being strict Subgroup of G
for g being Element of G st g in (carr G) . H holds
g " in (carr G) . H
proof end;

theorem Th23: :: LATSUBGR:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)
proof end;

theorem :: LATSUBGR:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being strict Subgroup of G holds (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)
proof end;

definition
let G be Group;
let F be non empty Subset of (Subgroups G);
func meet F -> strict Subgroup of G means :Def2: :: LATSUBGR:def 2
the carrier of it = meet ((carr G) .: F);
existence
ex b1 being strict Subgroup of G st the carrier of b1 = meet ((carr G) .: F)
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = meet ((carr G) .: F) & the carrier of b2 = meet ((carr G) .: F) holds
b1 = b2
by GROUP_2:68;
end;

:: deftheorem Def2 defines meet LATSUBGR:def 2 :
for G being Group
for F being non empty Subset of (Subgroups G)
for b3 being strict Subgroup of G holds
( b3 = meet F iff the carrier of b3 = meet ((carr G) .: F) );

theorem :: LATSUBGR:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for F being non empty Subset of (Subgroups G) st (1). G in F holds
meet F = (1). G
proof end;

theorem :: LATSUBGR:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for h being Element of Subgroups G
for F being non empty Subset of (Subgroups G) st F = {h} holds
meet F = h
proof end;

theorem Th27: :: LATSUBGR:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds
h1 "\/" h2 = H1 "\/" H2
proof end;

theorem Th28: :: LATSUBGR:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds
h1 "/\" h2 = H1 /\ H2
proof end;

theorem Th29: :: LATSUBGR:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for p being Element of (lattice G)
for H being Subgroup of G st p = H holds
H is strict Subgroup of G
proof end;

theorem Th30: :: LATSUBGR:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for p, q being Element of (lattice G) st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
proof end;

theorem :: LATSUBGR:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group
for H1, H2 being Subgroup of G
for p, q being Element of (lattice G) st p = H1 & q = H2 holds
( p [= q iff H1 is Subgroup of H2 )
proof end;

theorem :: LATSUBGR:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds lattice G is complete
proof end;

definition
let G1, G2 be Group;
let f be Function of the carrier of G1,the carrier of G2;
func FuncLatt f -> Function of the carrier of (lattice G1),the carrier of (lattice G2) means :Def3: :: LATSUBGR:def 3
for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
it . H = gr A;
existence
ex b1 being Function of the carrier of (lattice G1),the carrier of (lattice G2) st
for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
b1 . H = gr A
proof end;
uniqueness
for b1, b2 being Function of the carrier of (lattice G1),the carrier of (lattice G2) st ( for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
b1 . H = gr A ) & ( for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
b2 . H = gr A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines FuncLatt LATSUBGR:def 3 :
for G1, G2 being Group
for f being Function of the carrier of G1,the carrier of G2
for b4 being Function of the carrier of (lattice G1),the carrier of (lattice G2) holds
( b4 = FuncLatt f iff for H being strict Subgroup of G1
for A being Subset of G2 st A = f .: the carrier of H holds
b4 . H = gr A );

theorem :: LATSUBGR:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Group holds FuncLatt (id the carrier of G) = id the carrier of (lattice G)
proof end;

theorem :: LATSUBGR:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is one-to-one
proof end;

theorem :: LATSUBGR:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2 holds (FuncLatt f) . ((1). G1) = (1). G2
proof end;

theorem Th36: :: LATSUBGR:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2
proof end;

theorem Th37: :: LATSUBGR:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2 holds FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2
proof end;

theorem :: LATSUBGR:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being Group
for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is Homomorphism of lattice G1, lattice G2
proof end;