Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β πΎ β HL) |
2 | | simpl3 1193 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
3 | | eqid 2731 |
. . . . . . 7
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | pmodl42.s |
. . . . . . 7
β’ π = (PSubSpβπΎ) |
5 | 3, 4 | psubssat 38323 |
. . . . . 6
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
6 | 1, 2, 5 | syl2anc 584 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (AtomsβπΎ)) |
7 | | simpl2 1192 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
8 | 3, 4 | psubssat 38323 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
9 | 1, 7, 8 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (AtomsβπΎ)) |
10 | | simprl 769 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
11 | 3, 4 | psubssat 38323 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
12 | 1, 10, 11 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (AtomsβπΎ)) |
13 | | pmodl42.p |
. . . . . . 7
β’ + =
(+πβπΎ) |
14 | 3, 13 | paddssat 38383 |
. . . . . 6
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π + π) β (AtomsβπΎ)) |
15 | 1, 9, 12, 14 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β (AtomsβπΎ)) |
16 | | simprr 771 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β π) |
17 | 4, 13 | paddclN 38411 |
. . . . . 6
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) β π) |
18 | 1, 2, 16, 17 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β π) |
19 | 3, 4 | psubssat 38323 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β π β (AtomsβπΎ)) |
20 | 1, 16, 19 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (AtomsβπΎ)) |
21 | 3, 13 | sspadd1 38384 |
. . . . . 6
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β π β (π + π)) |
22 | 1, 6, 20, 21 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (π + π)) |
23 | 3, 4, 13 | pmod1i 38417 |
. . . . . 6
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ (π + π) β (AtomsβπΎ) β§ (π + π) β π)) β (π β (π + π) β ((π + (π + π)) β© (π + π)) = (π + ((π + π) β© (π + π))))) |
24 | 23 | 3impia 1117 |
. . . . 5
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ (π + π) β (AtomsβπΎ) β§ (π + π) β π) β§ π β (π + π)) β ((π + (π + π)) β© (π + π)) = (π + ((π + π) β© (π + π)))) |
25 | 1, 6, 15, 18, 22, 24 | syl131anc 1383 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + (π + π)) β© (π + π)) = (π + ((π + π) β© (π + π)))) |
26 | | incom 4181 |
. . . 4
β’ ((π + (π + π)) β© (π + π)) = ((π + π) β© (π + (π + π))) |
27 | 25, 26 | eqtr3di 2786 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + ((π + π) β© (π + π))) = ((π + π) β© (π + (π + π)))) |
28 | 27 | oveq2d 7393 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + (π + ((π + π) β© (π + π)))) = (π + ((π + π) β© (π + (π + π))))) |
29 | | ssinss1 4217 |
. . . 4
β’ ((π + π) β (AtomsβπΎ) β ((π + π) β© (π + π)) β (AtomsβπΎ)) |
30 | 15, 29 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) β© (π + π)) β (AtomsβπΎ)) |
31 | 3, 13 | paddass 38407 |
. . 3
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ ((π + π) β© (π + π)) β (AtomsβπΎ))) β ((π + π) + ((π + π) β© (π + π))) = (π + (π + ((π + π) β© (π + π))))) |
32 | 1, 9, 6, 30, 31 | syl13anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) + ((π + π) β© (π + π))) = (π + (π + ((π + π) β© (π + π))))) |
33 | 3, 13 | paddass 38407 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((π + π) + π) = (π + (π + π))) |
34 | 1, 9, 6, 12, 33 | syl13anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) |
35 | 3, 13 | padd12N 38408 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π + (π + π)) = (π + (π + π))) |
36 | 1, 9, 6, 12, 35 | syl13anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + (π + π)) = (π + (π + π))) |
37 | 34, 36 | eqtrd 2771 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) |
38 | 3, 13 | paddass 38407 |
. . . . . 6
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((π + π) + π) = (π + (π + π))) |
39 | 1, 9, 6, 20, 38 | syl13anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) |
40 | 37, 39 | ineq12d 4193 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π + π) + π) β© ((π + π) + π)) = ((π + (π + π)) β© (π + (π + π)))) |
41 | | incom 4181 |
. . . 4
β’ ((π + (π + π)) β© (π + (π + π))) = ((π + (π + π)) β© (π + (π + π))) |
42 | 40, 41 | eqtrdi 2787 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π + π) + π) β© ((π + π) + π)) = ((π + (π + π)) β© (π + (π + π)))) |
43 | 3, 4 | psubssat 38323 |
. . . . 5
β’ ((πΎ β HL β§ (π + π) β π) β (π + π) β (AtomsβπΎ)) |
44 | 1, 18, 43 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β (AtomsβπΎ)) |
45 | 4, 13 | paddclN 38411 |
. . . . . 6
β’ ((πΎ β HL β§ π β π β§ π β π) β (π + π) β π) |
46 | 1, 7, 10, 45 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β π) |
47 | 4, 13 | paddclN 38411 |
. . . . 5
β’ ((πΎ β HL β§ π β π β§ (π + π) β π) β (π + (π + π)) β π) |
48 | 1, 2, 46, 47 | syl3anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + (π + π)) β π) |
49 | 3, 13 | sspadd1 38384 |
. . . . . 6
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β π β (π + π)) |
50 | 1, 9, 12, 49 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (π + π)) |
51 | 3, 13 | sspadd2 38385 |
. . . . . 6
β’ ((πΎ β HL β§ (π + π) β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π + π) β (π + (π + π))) |
52 | 1, 15, 6, 51 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (π + π) β (π + (π + π))) |
53 | 50, 52 | sstrd 3972 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β π β (π + (π + π))) |
54 | 3, 4, 13 | pmod1i 38417 |
. . . . 5
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ (π + π) β (AtomsβπΎ) β§ (π + (π + π)) β π)) β (π β (π + (π + π)) β ((π + (π + π)) β© (π + (π + π))) = (π + ((π + π) β© (π + (π + π)))))) |
55 | 54 | 3impia 1117 |
. . . 4
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ (π + π) β (AtomsβπΎ) β§ (π + (π + π)) β π) β§ π β (π + (π + π))) β ((π + (π + π)) β© (π + (π + π))) = (π + ((π + π) β© (π + (π + π))))) |
56 | 1, 9, 44, 48, 53, 55 | syl131anc 1383 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ((π + (π + π)) β© (π + (π + π))) = (π + ((π + π) β© (π + (π + π))))) |
57 | 42, 56 | eqtrd 2771 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π + π) + π) β© ((π + π) + π)) = (π + ((π + π) β© (π + (π + π))))) |
58 | 28, 32, 57 | 3eqtr4rd 2782 |
1
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π + π) + π) β© ((π + π) + π)) = ((π + π) + ((π + π) β© (π + π)))) |