Metamath Proof Explorer


Theorem lsmcntz

Description: The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses lsmcntz.p
|- .(+) = ( LSSum ` G )
lsmcntz.s
|- ( ph -> S e. ( SubGrp ` G ) )
lsmcntz.t
|- ( ph -> T e. ( SubGrp ` G ) )
lsmcntz.u
|- ( ph -> U e. ( SubGrp ` G ) )
lsmcntz.z
|- Z = ( Cntz ` G )
Assertion lsmcntz
|- ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmcntz.p
 |-  .(+) = ( LSSum ` G )
2 lsmcntz.s
 |-  ( ph -> S e. ( SubGrp ` G ) )
3 lsmcntz.t
 |-  ( ph -> T e. ( SubGrp ` G ) )
4 lsmcntz.u
 |-  ( ph -> U e. ( SubGrp ` G ) )
5 lsmcntz.z
 |-  Z = ( Cntz ` G )
6 subgrcl
 |-  ( U e. ( SubGrp ` G ) -> G e. Grp )
7 eqid
 |-  ( Base ` G ) = ( Base ` G )
8 7 subgss
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
9 7 5 cntzsubg
 |-  ( ( G e. Grp /\ U C_ ( Base ` G ) ) -> ( Z ` U ) e. ( SubGrp ` G ) )
10 6 8 9 syl2anc
 |-  ( U e. ( SubGrp ` G ) -> ( Z ` U ) e. ( SubGrp ` G ) )
11 4 10 syl
 |-  ( ph -> ( Z ` U ) e. ( SubGrp ` G ) )
12 1 lsmlub
 |-  ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ ( Z ` U ) e. ( SubGrp ` G ) ) -> ( ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) <-> ( S .(+) T ) C_ ( Z ` U ) ) )
13 2 3 11 12 syl3anc
 |-  ( ph -> ( ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) <-> ( S .(+) T ) C_ ( Z ` U ) ) )
14 13 bicomd
 |-  ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )