Metamath Proof Explorer

Theorem lsmmod2

Description: Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 8-Jan-2015) (Revised by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis lsmmod.p 
|- .(+) = ( LSSum ` G )
Assertion lsmmod2 
|- ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> ( S i^i ( T .(+) U ) ) = ( ( S i^i T ) .(+) U ) )

Proof

Step Hyp Ref Expression
1 lsmmod.p 
 |-  .(+) = ( LSSum ` G )
2 simpl3 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> U e. ( SubGrp ` G ) )
3 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
4 3 oppgsubg 
 |-  ( SubGrp ` G ) = ( SubGrp ` ( oppG ` G ) )
5 2 4 eleqtrdi 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> U e. ( SubGrp ` ( oppG ` G ) ) )
6 simpl2 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> T e. ( SubGrp ` G ) )
7 6 4 eleqtrdi 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> T e. ( SubGrp ` ( oppG ` G ) ) )
8 simpl1 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> S e. ( SubGrp ` G ) )
9 8 4 eleqtrdi 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> S e. ( SubGrp ` ( oppG ` G ) ) )
10 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> U C_ S )
11 eqid 
 |-  ( LSSum ` ( oppG ` G ) ) = ( LSSum ` ( oppG ` G ) )
12 11 lsmmod 
 |-  ( ( ( U e. ( SubGrp ` ( oppG ` G ) ) /\ T e. ( SubGrp ` ( oppG ` G ) ) /\ S e. ( SubGrp ` ( oppG ` G ) ) ) /\ U C_ S ) -> ( U ( LSSum ` ( oppG ` G ) ) ( T i^i S ) ) = ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) )
13 5 7 9 10 12 syl31anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> ( U ( LSSum ` ( oppG ` G ) ) ( T i^i S ) ) = ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) )
14 13 eqcomd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) = ( U ( LSSum ` ( oppG ` G ) ) ( T i^i S ) ) )
15 incom 
 |-  ( ( U ( LSSum ` ( oppG ` G ) ) T ) i^i S ) = ( S i^i ( U ( LSSum ` ( oppG ` G ) ) T ) )
16 incom 
 |-  ( T i^i S ) = ( S i^i T )
17 16 oveq2i 
 |-  ( U ( LSSum ` ( oppG ` G ) ) ( T i^i S ) ) = ( U ( LSSum ` ( oppG ` G ) ) ( S i^i T ) )
18 14 15 17 3eqtr3g 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> ( S i^i ( U ( LSSum ` ( oppG ` G ) ) T ) ) = ( U ( LSSum ` ( oppG ` G ) ) ( S i^i T ) ) )
19 3 1 oppglsm 
 |-  ( U ( LSSum ` ( oppG ` G ) ) T ) = ( T .(+) U )
20 19 ineq2i 
 |-  ( S i^i ( U ( LSSum ` ( oppG ` G ) ) T ) ) = ( S i^i ( T .(+) U ) )
21 3 1 oppglsm 
 |-  ( U ( LSSum ` ( oppG ` G ) ) ( S i^i T ) ) = ( ( S i^i T ) .(+) U )
22 18 20 21 3eqtr3g 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ U C_ S ) -> ( S i^i ( T .(+) U ) ) = ( ( S i^i T ) .(+) U ) )