Step | Hyp | Ref
| Expression |
1 | | simpl11 1248 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β πΎ β HL) |
2 | | simpl12 1249 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β π΄) |
3 | | simpl13 1250 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β π΄) |
4 | | ssinss1 4217 |
. . . . 5
β’ (π β π΄ β (π β© π) β π΄) |
5 | 3, 4 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β (π β© π) β π΄) |
6 | | pmodlem.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
7 | | pmodlem.p |
. . . . 5
β’ + =
(+πβπΎ) |
8 | 6, 7 | sspadd1 38384 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (π β© π) β π΄) β π β (π + (π β© π))) |
9 | 1, 2, 5, 8 | syl3anc 1371 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β (π + (π β© π))) |
10 | | simpr 485 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π = π) |
11 | | simpl31 1254 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β π) |
12 | 10, 11 | eqeltrd 2832 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β π) |
13 | 9, 12 | sseldd 3963 |
. 2
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π = π) β π β (π + (π β© π))) |
14 | | simpl11 1248 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β πΎ β HL) |
15 | 14 | hllatd 37932 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β πΎ β Lat) |
16 | | simpl12 1249 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
17 | | simpl13 1250 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
18 | 17, 4 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β (π β© π) β π΄) |
19 | | simpl31 1254 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
20 | | simpl32 1255 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
21 | | simpl21 1251 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
22 | | simpl22 1252 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
23 | | simpl23 1253 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
24 | | pmodlem.s |
. . . . . . . . . 10
β’ π = (PSubSpβπΎ) |
25 | 6, 24 | psubssat 38323 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π) β π β π΄) |
26 | 14, 21, 25 | syl2anc 584 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
27 | 26, 23 | sseldd 3963 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
28 | 17, 20 | sseldd 3963 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
29 | 16, 19 | sseldd 3963 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π΄) |
30 | 27, 28, 29 | 3jca 1128 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β (π β π΄ β§ π β π΄ β§ π β π΄)) |
31 | | simpr 485 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
32 | | simpl33 1256 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β€ (π β¨ π)) |
33 | | pmodlem.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
34 | | pmodlem.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
35 | 33, 34, 6 | hlatexch1 37964 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
36 | 35 | imp 407 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
37 | 14, 30, 31, 32, 36 | syl31anc 1373 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β€ (π β¨ π)) |
38 | | simp31 1209 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
39 | 38 | snssd 4789 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β {π} β π) |
40 | | simp22 1207 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
41 | 39, 40 | sstrd 3972 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β {π} β π) |
42 | | simp23 1208 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
43 | 42 | snssd 4789 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β {π} β π) |
44 | | simp11 1203 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β πΎ β HL) |
45 | | simp12 1204 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
46 | 45, 38 | sseldd 3963 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
47 | 46 | snssd 4789 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β {π} β π΄) |
48 | | simp21 1206 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
49 | 44, 48, 25 | syl2anc 584 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
50 | 49, 42 | sseldd 3963 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
51 | 50 | snssd 4789 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β {π} β π΄) |
52 | 6, 24, 7 | paddss 38414 |
. . . . . . . 8
β’ ((πΎ β HL β§ ({π} β π΄ β§ {π} β π΄ β§ π β π)) β (({π} β π β§ {π} β π) β ({π} + {π}) β π)) |
53 | 44, 47, 51, 48, 52 | syl13anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β (({π} β π β§ {π} β π) β ({π} + {π}) β π)) |
54 | 41, 43, 53 | mpbi2and 710 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β ({π} + {π}) β π) |
55 | | simp33 1211 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β€ (π β¨ π)) |
56 | 44 | hllatd 37932 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β πΎ β Lat) |
57 | | simp13 1205 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
58 | | simp32 1210 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
59 | 57, 58 | sseldd 3963 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π΄) |
60 | 33, 34, 6, 7 | elpadd2at2 38376 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β ({π} + {π}) β π β€ (π β¨ π))) |
61 | 56, 46, 50, 59, 60 | syl13anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β (π β ({π} + {π}) β π β€ (π β¨ π))) |
62 | 55, 61 | mpbird 256 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β ({π} + {π})) |
63 | 54, 62 | sseldd 3963 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β π) |
64 | 14, 16, 17, 21, 22, 23, 19, 20, 37, 63 | syl333anc 1402 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β π) |
65 | 20, 64 | elind 4174 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β (π β© π)) |
66 | 33, 34, 6, 7 | elpaddri 38371 |
. . 3
β’ (((πΎ β Lat β§ π β π΄ β§ (π β© π) β π΄) β§ (π β π β§ π β (π β© π)) β§ (π β π΄ β§ π β€ (π β¨ π))) β π β (π + (π β© π))) |
67 | 15, 16, 18, 19, 65, 27, 32, 66 | syl322anc 1398 |
. 2
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β§ π β π) β π β (π + (π β© π))) |
68 | 13, 67 | pm2.61dane 3028 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β (π + (π β© π))) |