:: LATSUBGR semantic presentation

theorem Th1: :: LATSUBGR:1

for b₁ being Group
for b₂, b₃ being Subgroup of b₁ holds the carrier of (b₂ /\ b₃) = the carrier of b₂ /\ the carrier of b₃

proof end;

theorem Th2: :: LATSUBGR:2

for b₁ being Group
for b₂ being set holds
( b₂ in Subgroups b₁ iff ex b₃ being strict Subgroup of b₁ st b₂ = b₃ )

proof end;

theorem Th3: :: LATSUBGR:3

for b₁ being Group
for b₂ being Subset of b₁
for b₃ being strict Subgroup of b₁ st b₂ = the carrier of b₃ holds
gr b₂ = b₃

proof end;

theorem Th4: :: LATSUBGR:4

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄ being Subset of b₁ st b₄ = the carrier of b₂ \/ the carrier of b₃ holds
b₂ "\/" b₃ = gr b₄

proof end;

theorem Th5: :: LATSUBGR:5

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄ being Element of b₁ st ( b₄ in b₂ or b₄ in b₃ ) holds
b₄ in b₂ "\/" b₃

proof end;

theorem Th6: :: LATSUBGR:6

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂
for b₄ being Subgroup of b₁ ex b₅ being strict Subgroup of b₂ st the carrier of b₅ = b₃ .: the carrier of b₄

proof end;

theorem Th7: :: LATSUBGR:7

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂
for b₄ being Subgroup of b₂ ex b₅ being strict Subgroup of b₁ st the carrier of b₅ = b₃ " the carrier of b₄

proof end;

theorem Th8: :: LATSUBGR:8

canceled;

theorem Th9: :: LATSUBGR:9

canceled;

theorem Th10: :: LATSUBGR:10

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂
for b₄, b₅ being Subgroup of b₁
for b₆, b₇ being Subgroup of b₂ st the carrier of b₆ = b₃ .: the carrier of b₄ & the carrier of b₇ = b₃ .: the carrier of b₅ & b₄ is Subgroup of b₅ holds
b₆ is Subgroup of b₇

proof end;

theorem Th11: :: LATSUBGR:11

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂
for b₄, b₅ being Subgroup of b₂
for b₆, b₇ being Subgroup of b₁ st the carrier of b₆ = b₃ " the carrier of b₄ & the carrier of b₇ = b₃ " the carrier of b₅ & b₄ is Subgroup of b₅ holds
b₆ is Subgroup of b₇

proof end;

theorem Th12: :: LATSUBGR:12

for b₁, b₂ being Group
for b₃ being Function of the carrier of b₁,the carrier of b₂
for b₄ being Subset of b₁ holds b₃ .: b₄ c= b₃ .: the carrier of (gr b₄)

proof end;

theorem Th13: :: LATSUBGR:13

for b₁, b₂ being Group
for b₃, b₄ being Subgroup of b₁
for b₅ being Function of the carrier of b₁,the carrier of b₂
for b₆ being Subset of b₁ st b₆ = the carrier of b₃ \/ the carrier of b₄ holds
b₅ .: the carrier of (b₃ "\/" b₄) = b₅ .: the carrier of (gr b₆) by Th4;

theorem Th14: :: LATSUBGR:14

for b₁ being Group
for b₂ being Subset of b₁ st b₂ = {(1. b₁)} holds
gr b₂ = (1). b₁

proof end;

definition

let c₁ be Group;
func carr c₁ -> Function of Subgroups a₁, bool the carrier of a₁ means :Def1: :: LATSUBGR:def 1
for b₁ being strict Subgroup of a₁ holds a₂ . b₁ = the carrier of b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines carr LATSUBGR:def 1 :

theorem Th15: :: LATSUBGR:15

canceled;

theorem Th16: :: LATSUBGR:16

canceled;

theorem Th17: :: LATSUBGR:17

canceled;

theorem Th18: :: LATSUBGR:18

for b₁ being Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₁ holds
( b₃ in (carr b₁) . b₂ iff b₃ in b₂ )

proof end;

theorem Th19: :: LATSUBGR:19

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds 1. b₁ in (carr b₁) . b₂

proof end;

theorem Th20: :: LATSUBGR:20

for b₁ being Group
for b₂ being strict Subgroup of b₁ holds (carr b₁) . b₂ <> {}

proof end;

theorem Th21: :: LATSUBGR:21

for b₁ being Group
for b₂ being strict Subgroup of b₁
for b₃, b₄ being Element of b₁ st b₃ in (carr b₁) . b₂ & b₄ in (carr b₁) . b₂ holds
b₃ * b₄ in (carr b₁) . b₂

proof end;

theorem Th22: :: LATSUBGR:22

for b₁ being Group
for b₂ being strict Subgroup of b₁
for b₃ being Element of b₁ st b₃ in (carr b₁) . b₂ holds
b₃ " in (carr b₁) . b₂

proof end;

theorem Th23: :: LATSUBGR:23

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ holds the carrier of (b₂ /\ b₃) = ((carr b₁) . b₂) /\ ((carr b₁) . b₃)

proof end;

theorem Th24: :: LATSUBGR:24

for b₁ being Group
for b₂, b₃ being strict Subgroup of b₁ holds (carr b₁) . (b₂ /\ b₃) = ((carr b₁) . b₂) /\ ((carr b₁) . b₃)

proof end;

definition

let c₁ be Group;
let c₂ be non empty Subset of (Subgroups c₁);
func meet c₂ -> strict Subgroup of a₁ means :Def2: :: LATSUBGR:def 2
the carrier of a₃ = meet ((carr a₁) .: a₂);
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def2 defines meet LATSUBGR:def 2 :

theorem Th25: :: LATSUBGR:25

for b₁ being Group
for b₂ being non empty Subset of (Subgroups b₁) st (1). b₁ in b₂ holds
meet b₂ = (1). b₁

proof end;

theorem Th26: :: LATSUBGR:26

for b₁ being Group
for b₂ being Element of Subgroups b₁
for b₃ being non empty Subset of (Subgroups b₁) st b₃ = {b₂} holds
meet b₃ = b₂

proof end;

theorem Th27: :: LATSUBGR:27

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄, b₅ being Element of (lattice b₁) st b₄ = b₂ & b₅ = b₃ holds
b₄ "\/" b₅ = b₂ "\/" b₃

proof end;

theorem Th28: :: LATSUBGR:28

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄, b₅ being Element of (lattice b₁) st b₄ = b₂ & b₅ = b₃ holds
b₄ "/\" b₅ = b₂ /\ b₃

proof end;

theorem Th29: :: LATSUBGR:29

for b₁ being Group
for b₂ being Element of (lattice b₁)
for b₃ being Subgroup of b₁ st b₂ = b₃ holds
b₃ is strict Subgroup of b₁

proof end;

theorem Th30: :: LATSUBGR:30

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄, b₅ being Element of (lattice b₁) st b₄ = b₂ & b₅ = b₃ holds
( b₄ [= b₅ iff the carrier of b₂ c= the carrier of b₃ )

proof end;

theorem Th31: :: LATSUBGR:31

for b₁ being Group
for b₂, b₃ being Subgroup of b₁
for b₄, b₅ being Element of (lattice b₁) st b₄ = b₂ & b₅ = b₃ holds
( b₄ [= b₅ iff b₂ is Subgroup of b₃ )

proof end;

theorem Th32: :: LATSUBGR:32

for b₁ being Group holds lattice b₁ is complete

proof end;

definition

let c₁, c₂ be Group;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
func FuncLatt c₃ -> Function of the carrier of (lattice a₁),the carrier of (lattice a₂) means :Def3: :: LATSUBGR:def 3
for b₁ being strict Subgroup of a₁
for b₂ being Subset of a₂ st b₂ = a₃ .: the carrier of b₁ holds
a₄ . b₁ = gr b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines FuncLatt LATSUBGR:def 3 :

theorem Th33: :: LATSUBGR:33

for b₁ being Group holds FuncLatt (id the carrier of b₁) = id the carrier of (lattice b₁)

proof end;

theorem Th34: :: LATSUBGR:34

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is one-to-one holds
FuncLatt b₃ is one-to-one

proof end;

theorem Th35: :: LATSUBGR:35

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds (FuncLatt b₃) . ((1). b₁) = (1). b₂

proof end;

theorem Th36: :: LATSUBGR:36

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is one-to-one holds
FuncLatt b₃ is Semilattice-Homomorphism of lattice b₁, lattice b₂

proof end;

theorem Th37: :: LATSUBGR:37

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds FuncLatt b₃ is sup-Semilattice-Homomorphism of lattice b₁, lattice b₂

proof end;

theorem Th38: :: LATSUBGR:38

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is one-to-one holds
FuncLatt b₃ is Homomorphism of lattice b₁, lattice b₂

proof end;