This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )