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 | |
|
Assertion | lsmmod2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmmod.p | |
|
2 | simpl3 | |
|
3 | eqid | |
|
4 | 3 | oppgsubg | |
5 | 2 4 | eleqtrdi | |
6 | simpl2 | |
|
7 | 6 4 | eleqtrdi | |
8 | simpl1 | |
|
9 | 8 4 | eleqtrdi | |
10 | simpr | |
|
11 | eqid | |
|
12 | 11 | lsmmod | |
13 | 5 7 9 10 12 | syl31anc | |
14 | 13 | eqcomd | |
15 | incom | |
|
16 | incom | |
|
17 | 16 | oveq2i | |
18 | 14 15 17 | 3eqtr3g | |
19 | 3 1 | oppglsm | |
20 | 19 | ineq2i | |
21 | 3 1 | oppglsm | |
22 | 18 20 21 | 3eqtr3g | |