Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΎ β HL) |
2 | | hlop 37853 |
. . 3
β’ (πΎ β HL β πΎ β OP) |
3 | 1, 2 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΎ β OP) |
4 | 1 | hllatd 37855 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΎ β Lat) |
5 | | simp12l 1287 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β π΄) |
6 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΎ β HL β§ π β π»)) |
7 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΉ β π) |
8 | | simp22 1208 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΊ β π) |
9 | | cdlemg12.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
10 | | cdlemg12.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
11 | | cdlemg12.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
12 | | cdlemg12.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
13 | 9, 10, 11, 12 | ltrncoat 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) |
14 | 6, 7, 8, 5, 13 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π΄) |
15 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
16 | | cdlemg12.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
17 | 15, 16, 10 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
18 | 1, 5, 14, 17 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
19 | | simp13l 1289 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β π΄) |
20 | 9, 10, 11, 12 | ltrncoat 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) |
21 | 6, 7, 8, 19, 20 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π΄) |
22 | 15, 16, 10 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
23 | 1, 19, 21, 22 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
24 | | cdlemg12.m |
. . . 4
β’ β§ =
(meetβπΎ) |
25 | 15, 24 | latmcl 18336 |
. . 3
β’ ((πΎ β Lat β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (BaseβπΎ)) |
26 | 4, 18, 23, 25 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (BaseβπΎ)) |
27 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
28 | | simp13 1206 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | | simp33 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π)) |
30 | 9, 16, 24, 10, 11, 12 | cdlemg11a 39129 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π) |
31 | 30 | necomd 3000 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β (πΉβ(πΊβπ))) |
32 | 6, 27, 28, 7, 8, 29, 31 | syl123anc 1388 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β (πΉβ(πΊβπ))) |
33 | 9, 16, 24, 10, 11 | lhpat 38535 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ ((πΉβ(πΊβπ)) β π΄ β§ π β (πΉβ(πΊβπ)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) β π΄) |
34 | 6, 27, 14, 32, 33 | syl112anc 1375 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) β π΄) |
35 | 16, 10 | hlatjcom 37859 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) |
36 | 1, 5, 14, 35 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) |
37 | 16, 10 | hlatjcom 37859 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) |
38 | 1, 19, 21, 37 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) |
39 | 36, 38 | oveq12d 7380 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π))) |
40 | | simp1 1137 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
41 | | simp2 1138 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉ β π β§ πΊ β π β§ π β π)) |
42 | | simp31l 1297 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β Β¬ (π
βπΉ) β€ (π β¨ π)) |
43 | | simp31r 1298 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β Β¬ (π
βπΊ) β€ (π β¨ π)) |
44 | | simp32 1211 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π
βπΉ) β (π
βπΊ)) |
45 | | cdlemg12b.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
46 | | eqid 2737 |
. . . . 5
β’
(0.βπΎ) =
(0.βπΎ) |
47 | 9, 16, 24, 10, 11, 12, 45, 46 | cdlemg12e 39139 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β (0.βπΎ)) |
48 | 40, 41, 42, 43, 44, 47 | syl113anc 1383 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β (0.βπΎ)) |
49 | 39, 48 | eqnetrd 3012 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (0.βπΎ)) |
50 | 9, 16, 24, 10, 11, 12, 45 | cdlemg12f 39140 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
51 | 15, 9, 46, 10 | leat2 37785 |
. 2
β’ (((πΎ β OP β§ ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (BaseβπΎ) β§ ((π β¨ (πΉβ(πΊβπ))) β§ π) β π΄) β§ (((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (0.βπΎ) β§ ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π β¨ (πΉβ(πΊβπ))) β§ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
52 | 3, 26, 34, 49, 50, 51 | syl32anc 1379 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β§ (π
βπΉ) β (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |