Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | simp2 1138 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (π β π΅ β§ Β¬ π β€ π)) |
3 | | simp3ll 1245 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β π β π΅) |
4 | | simp3r 1203 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (π β§ π) β€ π) |
5 | | dihmeetlem14.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
6 | | dihmeetlem14.l |
. . . 4
β’ β€ =
(leβπΎ) |
7 | | dihmeetlem14.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
8 | | dihmeetlem14.m |
. . . 4
β’ β§ =
(meetβπΎ) |
9 | | dihmeetlem14.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
10 | | dihmeetlem14.h |
. . . 4
β’ π» = (LHypβπΎ) |
11 | 5, 6, 7, 8, 9, 10 | lhpmcvr6N 38541 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) |
12 | 1, 2, 3, 4, 11 | syl112anc 1375 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) |
13 | | simp3l 1202 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (π β π΅ β§ Β¬ π β€ π)) |
14 | | simp2l 1200 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β π β π΅) |
15 | | simp1l 1198 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β πΎ β HL) |
16 | 15 | hllatd 37876 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β πΎ β Lat) |
17 | 5, 8 | latmcom 18360 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) |
18 | 16, 3, 14, 17 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (π β§ π) = (π β§ π)) |
19 | 18, 4 | eqbrtrd 5131 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (π β§ π) β€ π) |
20 | 5, 6, 7, 8, 9, 10 | lhpmcvr6N 38541 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) |
21 | 1, 13, 14, 19, 20 | syl112anc 1375 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) |
22 | | reeanv 3216 |
. . 3
β’
(βπ β
π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) β (βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) |
23 | | simp11 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (πΎ β HL β§ π β π»)) |
24 | | simp12 1205 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (π β π΅ β§ Β¬ π β€ π)) |
25 | 3 | 3ad2ant1 1134 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β π β π΅) |
26 | | simp2l 1200 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β π β π΄) |
27 | | simp3l1 1279 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β Β¬ π β€ π) |
28 | 26, 27 | jca 513 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | | simp2r 1201 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β π β π΄) |
30 | | simp3r1 1282 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β Β¬ π β€ π) |
31 | 29, 30 | jca 513 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (π β π΄ β§ Β¬ π β€ π)) |
32 | | simp3l3 1281 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β π β€ π) |
33 | | simp3r3 1284 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β π β€ π) |
34 | | simp13r 1290 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (π β§ π) β€ π) |
35 | 32, 33, 34 | 3jca 1129 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (π β€ π β§ π β€ π β§ (π β§ π) β€ π)) |
36 | | dihmeetlem14.u |
. . . . . . 7
β’ π = ((DVecHβπΎ)βπ) |
37 | | dihmeetlem14.s |
. . . . . . 7
β’ β =
(LSSumβπ) |
38 | | dihmeetlem14.i |
. . . . . . 7
β’ πΌ = ((DIsoHβπΎ)βπ) |
39 | 5, 6, 10, 7, 8, 9,
36, 37, 38 | dihmeetlem19N 39838 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ π β€ π β§ (π β§ π) β€ π))) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) |
40 | 23, 24, 25, 28, 31, 35, 39 | syl33anc 1386 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β§ (π β π΄ β§ π β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π))) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) |
41 | 40 | 3exp 1120 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β ((π β π΄ β§ π β π΄) β (((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))))) |
42 | 41 | rexlimdvv 3201 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ)))) |
43 | 22, 42 | biimtrrid 242 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β ((βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π) β§ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ)))) |
44 | 12, 21, 43 | mp2and 698 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β§ π) β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) |