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 ˙=LSSumG
Assertion lsmmod2 SSubGrpGTSubGrpGUSubGrpGUSST˙U=ST˙U

Proof

Step Hyp Ref Expression
1 lsmmod.p ˙=LSSumG
2 simpl3 SSubGrpGTSubGrpGUSubGrpGUSUSubGrpG
3 eqid opp𝑔G=opp𝑔G
4 3 oppgsubg SubGrpG=SubGrpopp𝑔G
5 2 4 eleqtrdi SSubGrpGTSubGrpGUSubGrpGUSUSubGrpopp𝑔G
6 simpl2 SSubGrpGTSubGrpGUSubGrpGUSTSubGrpG
7 6 4 eleqtrdi SSubGrpGTSubGrpGUSubGrpGUSTSubGrpopp𝑔G
8 simpl1 SSubGrpGTSubGrpGUSubGrpGUSSSubGrpG
9 8 4 eleqtrdi SSubGrpGTSubGrpGUSubGrpGUSSSubGrpopp𝑔G
10 simpr SSubGrpGTSubGrpGUSubGrpGUSUS
11 eqid LSSumopp𝑔G=LSSumopp𝑔G
12 11 lsmmod USubGrpopp𝑔GTSubGrpopp𝑔GSSubGrpopp𝑔GUSULSSumopp𝑔GTS=ULSSumopp𝑔GTS
13 5 7 9 10 12 syl31anc SSubGrpGTSubGrpGUSubGrpGUSULSSumopp𝑔GTS=ULSSumopp𝑔GTS
14 13 eqcomd SSubGrpGTSubGrpGUSubGrpGUSULSSumopp𝑔GTS=ULSSumopp𝑔GTS
15 incom ULSSumopp𝑔GTS=SULSSumopp𝑔GT
16 incom TS=ST
17 16 oveq2i ULSSumopp𝑔GTS=ULSSumopp𝑔GST
18 14 15 17 3eqtr3g SSubGrpGTSubGrpGUSubGrpGUSSULSSumopp𝑔GT=ULSSumopp𝑔GST
19 3 1 oppglsm ULSSumopp𝑔GT=T˙U
20 19 ineq2i SULSSumopp𝑔GT=ST˙U
21 3 1 oppglsm ULSSumopp𝑔GST=ST˙U
22 18 20 21 3eqtr3g SSubGrpGTSubGrpGUSubGrpGUSST˙U=ST˙U