Step | Hyp | Ref
| Expression |
1 | | cdlemk5.z |
. . 3
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
2 | 1 | oveq1i 7368 |
. 2
β’ (π β¨ (π
βπ)) = (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
βπ)) |
3 | | simp1l 1198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β πΎ β HL) |
4 | | simp1 1137 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (πΎ β HL β§ π β π»)) |
5 | | simp3rl 1247 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β π β π) |
6 | | simp3rr 1248 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β π β ( I βΎ π΅)) |
7 | | cdlemk5.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
8 | | cdlemk5.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
9 | | cdlemk5.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
10 | | cdlemk5.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
11 | | cdlemk5.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
12 | 7, 8, 9, 10, 11 | trlnidat 38682 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β ( I βΎ π΅)) β (π
βπ) β π΄) |
13 | 4, 5, 6, 12 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
βπ) β π΄) |
14 | | simp3ll 1245 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β π β π΄) |
15 | | cdlemk5.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
16 | 7, 15, 8 | hlatjcl 37875 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπ) β π΄) β (π β¨ (π
βπ)) β π΅) |
17 | 3, 14, 13, 16 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β¨ (π
βπ)) β π΅) |
18 | 3 | hllatd 37872 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β πΎ β Lat) |
19 | | simp22 1208 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β π β π) |
20 | 7, 8 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
21 | 14, 20 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β π β π΅) |
22 | 7, 9, 10 | ltrncl 38634 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΅) β (πβπ) β π΅) |
23 | 4, 19, 21, 22 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (πβπ) β π΅) |
24 | | simp21 1207 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β πΉ β π) |
25 | 9, 10 | ltrncnv 38655 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
26 | 4, 24, 25 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β β‘πΉ β π) |
27 | 9, 10 | ltrnco 39228 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΉ β π) β (π β β‘πΉ) β π) |
28 | 4, 5, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β β‘πΉ) β π) |
29 | 7, 9, 10, 11 | trlcl 38673 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β β‘πΉ) β π) β (π
β(π β β‘πΉ)) β π΅) |
30 | 4, 28, 29 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
β(π β β‘πΉ)) β π΅) |
31 | 7, 15 | latjcl 18333 |
. . . . 5
β’ ((πΎ β Lat β§ (πβπ) β π΅ β§ (π
β(π β β‘πΉ)) β π΅) β ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) |
32 | 18, 23, 30, 31 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) |
33 | | cdlemk5.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
34 | 33, 15, 8 | hlatlej2 37884 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπ) β π΄) β (π
βπ) β€ (π β¨ (π
βπ))) |
35 | 3, 14, 13, 34 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
βπ) β€ (π β¨ (π
βπ))) |
36 | | cdlemk5.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
37 | 7, 33, 15, 36, 8 | atmod2i1 38370 |
. . . 4
β’ ((πΎ β HL β§ ((π
βπ) β π΄ β§ (π β¨ (π
βπ)) β π΅ β§ ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) β§ (π
βπ) β€ (π β¨ (π
βπ))) β (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
βπ)) = ((π β¨ (π
βπ)) β§ (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)))) |
38 | 3, 13, 17, 32, 35, 37 | syl131anc 1384 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
βπ)) = ((π β¨ (π
βπ)) β§ (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)))) |
39 | 7, 8 | atbase 37797 |
. . . . . . . 8
β’ ((π
βπ) β π΄ β (π
βπ) β π΅) |
40 | 13, 39 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
βπ) β π΅) |
41 | 7, 9, 10, 11 | trlcl 38673 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π
βπ) β π΅) |
42 | 4, 19, 41 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
βπ) β π΅) |
43 | 7, 15 | latj32 18379 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β π΅ β§ (π
βπ) β π΅ β§ (π
βπ) β π΅)) β ((π β¨ (π
βπ)) β¨ (π
βπ)) = ((π β¨ (π
βπ)) β¨ (π
βπ))) |
44 | 18, 21, 40, 42, 43 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β¨ (π
βπ)) = ((π β¨ (π
βπ)) β¨ (π
βπ))) |
45 | | simp3l 1202 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β π΄ β§ Β¬ π β€ π)) |
46 | 33, 15, 8, 9, 10, 11 | trljat3 38677 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπ)) = ((πβπ) β¨ (π
βπ))) |
47 | 4, 19, 45, 46 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β¨ (π
βπ)) = ((πβπ) β¨ (π
βπ))) |
48 | 47 | oveq1d 7373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β¨ (π
βπ)) = (((πβπ) β¨ (π
βπ)) β¨ (π
βπ))) |
49 | 7, 15 | latjass 18377 |
. . . . . . 7
β’ ((πΎ β Lat β§ ((πβπ) β π΅ β§ (π
βπ) β π΅ β§ (π
βπ) β π΅)) β (((πβπ) β¨ (π
βπ)) β¨ (π
βπ)) = ((πβπ) β¨ ((π
βπ) β¨ (π
βπ)))) |
50 | 18, 23, 42, 40, 49 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (((πβπ) β¨ (π
βπ)) β¨ (π
βπ)) = ((πβπ) β¨ ((π
βπ) β¨ (π
βπ)))) |
51 | 44, 48, 50 | 3eqtrd 2777 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β¨ (π
βπ)) = ((πβπ) β¨ ((π
βπ) β¨ (π
βπ)))) |
52 | 7, 15 | latjass 18377 |
. . . . . . 7
β’ ((πΎ β Lat β§ ((πβπ) β π΅ β§ (π
β(π β β‘πΉ)) β π΅ β§ (π
βπ) β π΅)) β (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)) = ((πβπ) β¨ ((π
β(π β β‘πΉ)) β¨ (π
βπ)))) |
53 | 18, 23, 30, 40, 52 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)) = ((πβπ) β¨ ((π
β(π β β‘πΉ)) β¨ (π
βπ)))) |
54 | 7, 15 | latjcom 18341 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π
βπ) β π΅ β§ (π
βπ) β π΅) β ((π
βπ) β¨ (π
βπ)) = ((π
βπ) β¨ (π
βπ))) |
55 | 18, 42, 40, 54 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
βπ)) = ((π
βπ) β¨ (π
βπ))) |
56 | 9, 10, 11 | trlcnv 38674 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
ββ‘πΉ) = (π
βπΉ)) |
57 | 4, 24, 56 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
ββ‘πΉ) = (π
βπΉ)) |
58 | | simp23 1209 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
βπΉ) = (π
βπ)) |
59 | 57, 58 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π
ββ‘πΉ) = (π
βπ)) |
60 | 59 | oveq2d 7374 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
ββ‘πΉ)) = ((π
βπ) β¨ (π
βπ))) |
61 | 55, 60 | eqtr4d 2776 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
βπ)) = ((π
βπ) β¨ (π
ββ‘πΉ))) |
62 | 15, 9, 10, 11 | trljco 39249 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΉ β π) β ((π
βπ) β¨ (π
β(π β β‘πΉ))) = ((π
βπ) β¨ (π
ββ‘πΉ))) |
63 | 4, 5, 26, 62 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
β(π β β‘πΉ))) = ((π
βπ) β¨ (π
ββ‘πΉ))) |
64 | 7, 15 | latjcom 18341 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π
βπ) β π΅ β§ (π
β(π β β‘πΉ)) β π΅) β ((π
βπ) β¨ (π
β(π β β‘πΉ))) = ((π
β(π β β‘πΉ)) β¨ (π
βπ))) |
65 | 18, 40, 30, 64 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
β(π β β‘πΉ))) = ((π
β(π β β‘πΉ)) β¨ (π
βπ))) |
66 | 61, 63, 65 | 3eqtr2d 2779 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π
βπ) β¨ (π
βπ)) = ((π
β(π β β‘πΉ)) β¨ (π
βπ))) |
67 | 66 | oveq2d 7374 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((πβπ) β¨ ((π
βπ) β¨ (π
βπ))) = ((πβπ) β¨ ((π
β(π β β‘πΉ)) β¨ (π
βπ)))) |
68 | 53, 67 | eqtr4d 2776 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)) = ((πβπ) β¨ ((π
βπ) β¨ (π
βπ)))) |
69 | 51, 68 | eqtr4d 2776 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β¨ (π
βπ)) = (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ))) |
70 | 69 | oveq2d 7374 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β§ ((π β¨ (π
βπ)) β¨ (π
βπ))) = ((π β¨ (π
βπ)) β§ (((πβπ) β¨ (π
β(π β β‘πΉ))) β¨ (π
βπ)))) |
71 | 7, 15, 36 | latabs2 18370 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ (π
βπ)) β π΅ β§ (π
βπ) β π΅) β ((π β¨ (π
βπ)) β§ ((π β¨ (π
βπ)) β¨ (π
βπ))) = (π β¨ (π
βπ))) |
72 | 18, 17, 42, 71 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β ((π β¨ (π
βπ)) β§ ((π β¨ (π
βπ)) β¨ (π
βπ))) = (π β¨ (π
βπ))) |
73 | 38, 70, 72 | 3eqtr2d 2779 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β¨ (π
βπ)) = (π β¨ (π
βπ))) |
74 | 2, 73 | eqtrid 2785 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π
βπΉ) = (π
βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β¨ (π
βπ)) = (π β¨ (π
βπ))) |