Metamath Proof Explorer


Theorem pmodl42N

Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmodl42.s S=PSubSpK
pmodl42.p +˙=+𝑃K
Assertion pmodl42N KHLXSYSZSWSX+˙Y+˙ZX+˙Y+˙W=X+˙Y+˙X+˙ZY+˙W

Proof

Step Hyp Ref Expression
1 pmodl42.s S=PSubSpK
2 pmodl42.p +˙=+𝑃K
3 simpl1 KHLXSYSZSWSKHL
4 simpl3 KHLXSYSZSWSYS
5 eqid AtomsK=AtomsK
6 5 1 psubssat KHLYSYAtomsK
7 3 4 6 syl2anc KHLXSYSZSWSYAtomsK
8 simpl2 KHLXSYSZSWSXS
9 5 1 psubssat KHLXSXAtomsK
10 3 8 9 syl2anc KHLXSYSZSWSXAtomsK
11 simprl KHLXSYSZSWSZS
12 5 1 psubssat KHLZSZAtomsK
13 3 11 12 syl2anc KHLXSYSZSWSZAtomsK
14 5 2 paddssat KHLXAtomsKZAtomsKX+˙ZAtomsK
15 3 10 13 14 syl3anc KHLXSYSZSWSX+˙ZAtomsK
16 simprr KHLXSYSZSWSWS
17 1 2 paddclN KHLYSWSY+˙WS
18 3 4 16 17 syl3anc KHLXSYSZSWSY+˙WS
19 5 1 psubssat KHLWSWAtomsK
20 3 16 19 syl2anc KHLXSYSZSWSWAtomsK
21 5 2 sspadd1 KHLYAtomsKWAtomsKYY+˙W
22 3 7 20 21 syl3anc KHLXSYSZSWSYY+˙W
23 5 1 2 pmod1i KHLYAtomsKX+˙ZAtomsKY+˙WSYY+˙WY+˙X+˙ZY+˙W=Y+˙X+˙ZY+˙W
24 23 3impia KHLYAtomsKX+˙ZAtomsKY+˙WSYY+˙WY+˙X+˙ZY+˙W=Y+˙X+˙ZY+˙W
25 3 7 15 18 22 24 syl131anc KHLXSYSZSWSY+˙X+˙ZY+˙W=Y+˙X+˙ZY+˙W
26 incom Y+˙X+˙ZY+˙W=Y+˙WY+˙X+˙Z
27 25 26 eqtr3di KHLXSYSZSWSY+˙X+˙ZY+˙W=Y+˙WY+˙X+˙Z
28 27 oveq2d KHLXSYSZSWSX+˙Y+˙X+˙ZY+˙W=X+˙Y+˙WY+˙X+˙Z
29 ssinss1 X+˙ZAtomsKX+˙ZY+˙WAtomsK
30 15 29 syl KHLXSYSZSWSX+˙ZY+˙WAtomsK
31 5 2 paddass KHLXAtomsKYAtomsKX+˙ZY+˙WAtomsKX+˙Y+˙X+˙ZY+˙W=X+˙Y+˙X+˙ZY+˙W
32 3 10 7 30 31 syl13anc KHLXSYSZSWSX+˙Y+˙X+˙ZY+˙W=X+˙Y+˙X+˙ZY+˙W
33 5 2 paddass KHLXAtomsKYAtomsKZAtomsKX+˙Y+˙Z=X+˙Y+˙Z
34 3 10 7 13 33 syl13anc KHLXSYSZSWSX+˙Y+˙Z=X+˙Y+˙Z
35 5 2 padd12N KHLXAtomsKYAtomsKZAtomsKX+˙Y+˙Z=Y+˙X+˙Z
36 3 10 7 13 35 syl13anc KHLXSYSZSWSX+˙Y+˙Z=Y+˙X+˙Z
37 34 36 eqtrd KHLXSYSZSWSX+˙Y+˙Z=Y+˙X+˙Z
38 5 2 paddass KHLXAtomsKYAtomsKWAtomsKX+˙Y+˙W=X+˙Y+˙W
39 3 10 7 20 38 syl13anc KHLXSYSZSWSX+˙Y+˙W=X+˙Y+˙W
40 37 39 ineq12d KHLXSYSZSWSX+˙Y+˙ZX+˙Y+˙W=Y+˙X+˙ZX+˙Y+˙W
41 incom Y+˙X+˙ZX+˙Y+˙W=X+˙Y+˙WY+˙X+˙Z
42 40 41 eqtrdi KHLXSYSZSWSX+˙Y+˙ZX+˙Y+˙W=X+˙Y+˙WY+˙X+˙Z
43 5 1 psubssat KHLY+˙WSY+˙WAtomsK
44 3 18 43 syl2anc KHLXSYSZSWSY+˙WAtomsK
45 1 2 paddclN KHLXSZSX+˙ZS
46 3 8 11 45 syl3anc KHLXSYSZSWSX+˙ZS
47 1 2 paddclN KHLYSX+˙ZSY+˙X+˙ZS
48 3 4 46 47 syl3anc KHLXSYSZSWSY+˙X+˙ZS
49 5 2 sspadd1 KHLXAtomsKZAtomsKXX+˙Z
50 3 10 13 49 syl3anc KHLXSYSZSWSXX+˙Z
51 5 2 sspadd2 KHLX+˙ZAtomsKYAtomsKX+˙ZY+˙X+˙Z
52 3 15 7 51 syl3anc KHLXSYSZSWSX+˙ZY+˙X+˙Z
53 50 52 sstrd KHLXSYSZSWSXY+˙X+˙Z
54 5 1 2 pmod1i KHLXAtomsKY+˙WAtomsKY+˙X+˙ZSXY+˙X+˙ZX+˙Y+˙WY+˙X+˙Z=X+˙Y+˙WY+˙X+˙Z
55 54 3impia KHLXAtomsKY+˙WAtomsKY+˙X+˙ZSXY+˙X+˙ZX+˙Y+˙WY+˙X+˙Z=X+˙Y+˙WY+˙X+˙Z
56 3 10 44 48 53 55 syl131anc KHLXSYSZSWSX+˙Y+˙WY+˙X+˙Z=X+˙Y+˙WY+˙X+˙Z
57 42 56 eqtrd KHLXSYSZSWSX+˙Y+˙ZX+˙Y+˙W=X+˙Y+˙WY+˙X+˙Z
58 28 32 57 3eqtr4rd KHLXSYSZSWSX+˙Y+˙ZX+˙Y+˙W=X+˙Y+˙X+˙ZY+˙W