Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π = β
) |
2 | 1 | oveq1d 7373 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π + π) = (β
+ π)) |
3 | | simpl1 1192 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β πΎ β HL) |
4 | | simpl22 1253 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π β π΄) |
5 | | pmodlem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
6 | | pmodlem.p |
. . . . . . 7
β’ + =
(+πβπΎ) |
7 | 5, 6 | padd02 38321 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β (β
+ π) = π) |
8 | 3, 4, 7 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (β
+ π) = π) |
9 | 2, 8 | eqtrd 2773 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π + π) = π) |
10 | 9 | ineq1d 4172 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β ((π + π) β© π) = (π β© π)) |
11 | | ssinss1 4198 |
. . . . 5
β’ (π β π΄ β (π β© π) β π΄) |
12 | 4, 11 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π β© π) β π΄) |
13 | | simpl21 1252 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π β π΄) |
14 | 5, 6 | sspadd2 38325 |
. . . 4
β’ ((πΎ β HL β§ (π β© π) β π΄ β§ π β π΄) β (π β© π) β (π + (π β© π))) |
15 | 3, 12, 13, 14 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π β© π) β (π + (π β© π))) |
16 | 10, 15 | eqsstrd 3983 |
. 2
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β ((π + π) β© π) β (π + (π β© π))) |
17 | | oveq2 7366 |
. . . . 5
β’ (π = β
β (π + π) = (π + β
)) |
18 | | simp1 1137 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β πΎ β HL) |
19 | | simp21 1207 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β π β π΄) |
20 | 5, 6 | padd01 38320 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β (π + β
) = π) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β (π + β
) = π) |
22 | 17, 21 | sylan9eqr 2795 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π + π) = π) |
23 | 22 | ineq1d 4172 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β ((π + π) β© π) = (π β© π)) |
24 | | inss1 4189 |
. . . 4
β’ (π β© π) β π |
25 | | simpl1 1192 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β πΎ β HL) |
26 | | simpl21 1252 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π β π΄) |
27 | | simpl22 1253 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π β π΄) |
28 | 27, 11 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π β© π) β π΄) |
29 | 5, 6 | sspadd1 38324 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π β© π) β π΄) β π β (π + (π β© π))) |
30 | 25, 26, 28, 29 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β π β (π + (π β© π))) |
31 | 24, 30 | sstrid 3956 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β (π β© π) β (π + (π β© π))) |
32 | 23, 31 | eqsstrd 3983 |
. 2
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π = β
) β ((π + π) β© π) β (π + (π β© π))) |
33 | | elin 3927 |
. . . 4
β’ (π β ((π + π) β© π) β (π β (π + π) β§ π β π)) |
34 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β πΎ β HL) |
35 | 34 | hllatd 37872 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β πΎ β Lat) |
36 | | simpl21 1252 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β π β π΄) |
37 | | simpl22 1253 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β π β π΄) |
38 | | simprl 770 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β (π β β
β§ π β β
)) |
39 | | pmodlem.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
40 | | pmodlem.j |
. . . . . . . . . 10
β’ β¨ =
(joinβπΎ) |
41 | 39, 40, 5, 6 | elpaddn0 38309 |
. . . . . . . . 9
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β β
)) β (π β (π + π) β (π β π΄ β§ βπ β π βπ β π π β€ (π β¨ π)))) |
42 | 35, 36, 37, 38, 41 | syl31anc 1374 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β (π β (π + π) β (π β π΄ β§ βπ β π βπ β π π β€ (π β¨ π)))) |
43 | | simpl1 1192 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β πΎ β HL) |
44 | | simpl21 1252 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π΄) |
45 | | simpl22 1253 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π΄) |
46 | | simpl23 1254 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π) |
47 | | simpl3 1194 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π) |
48 | | simpr1 1195 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π) |
49 | | simpr2l 1233 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π) |
50 | | simpr2r 1234 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β π) |
51 | | simpr3 1197 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β€ (π β¨ π)) |
52 | | pmodlem.s |
. . . . . . . . . . . . . . 15
β’ π = (PSubSpβπΎ) |
53 | 39, 40, 5, 52, 6 | pmodlem1 38355 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β (π + (π β© π))) |
54 | 43, 44, 45, 46, 47, 48, 49, 50, 51, 53 | syl333anc 1403 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β π β§ (π β π β§ π β π) β§ π β€ (π β¨ π))) β π β (π + (π β© π))) |
55 | 54 | 3exp2 1355 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β (π β π β ((π β π β§ π β π) β (π β€ (π β¨ π) β π β (π + (π β© π)))))) |
56 | 55 | imp 408 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π β π) β ((π β π β§ π β π) β (π β€ (π β¨ π) β π β (π + (π β© π))))) |
57 | 56 | rexlimdvv 3201 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π β π) β (βπ β π βπ β π π β€ (π β¨ π) β π β (π + (π β© π)))) |
58 | 57 | adantld 492 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ π β π) β ((π β π΄ β§ βπ β π βπ β π π β€ (π β¨ π)) β π β (π + (π β© π)))) |
59 | 58 | adantrl 715 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β ((π β π΄ β§ βπ β π βπ β π π β€ (π β¨ π)) β π β (π + (π β© π)))) |
60 | 42, 59 | sylbid 239 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ ((π β β
β§ π β β
) β§ π β π)) β (π β (π + π) β π β (π + (π β© π)))) |
61 | 60 | exp32 422 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π β β
β§ π β β
) β (π β π β (π β (π + π) β π β (π + (π β© π)))))) |
62 | 61 | com34 91 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π β β
β§ π β β
) β (π β (π + π) β (π β π β π β (π + (π β© π)))))) |
63 | 62 | imp4b 423 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β β
β§ π β β
)) β ((π β (π + π) β§ π β π) β π β (π + (π β© π)))) |
64 | 33, 63 | biimtrid 241 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β β
β§ π β β
)) β (π β ((π + π) β© π) β π β (π + (π β© π)))) |
65 | 64 | ssrdv 3951 |
. 2
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β§ (π β β
β§ π β β
)) β ((π + π) β© π) β (π + (π β© π))) |
66 | 16, 32, 65 | pm2.61da2ne 3030 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π + π) β© π) β (π + (π β© π))) |