Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (πΎ β HL β§ π β π»)) |
2 | | hlclat 37823 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
3 | 2 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β πΎ β CLat) |
4 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | eqid 2737 |
. . . . . . . . . 10
β’
(leβπΎ) =
(leβπΎ) |
6 | | diaglb.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
7 | | diaglb.i |
. . . . . . . . . 10
β’ πΌ = ((DIsoAβπΎ)βπ) |
8 | 4, 5, 6, 7 | diadm 39501 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β dom πΌ = {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π}) |
9 | 8 | sseq2d 3977 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (π β dom πΌ β π β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π})) |
10 | 9 | biimpa 478 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π}) |
11 | 10 | adantrr 716 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β π β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π}) |
12 | | ssrab2 4038 |
. . . . . 6
β’ {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} β (BaseβπΎ) |
13 | 11, 12 | sstrdi 3957 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β π β (BaseβπΎ)) |
14 | | diaglb.g |
. . . . . 6
β’ πΊ = (glbβπΎ) |
15 | 4, 14 | clatglbcl 18395 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β (πΊβπ) β (BaseβπΎ)) |
16 | 3, 13, 15 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (πΊβπ) β (BaseβπΎ)) |
17 | | simprr 772 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β π β β
) |
18 | | n0 4307 |
. . . . . 6
β’ (π β β
β
βπ₯ π₯ β π) |
19 | 17, 18 | sylib 217 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β βπ₯ π₯ β π) |
20 | | hllat 37828 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
21 | 20 | ad3antrrr 729 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β πΎ β Lat) |
22 | 16 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (πΊβπ) β (BaseβπΎ)) |
23 | | ssel2 3940 |
. . . . . . . . . 10
β’ ((π β dom πΌ β§ π₯ β π) β π₯ β dom πΌ) |
24 | 23 | adantlr 714 |
. . . . . . . . 9
β’ (((π β dom πΌ β§ π β β
) β§ π₯ β π) β π₯ β dom πΌ) |
25 | 24 | adantll 713 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π₯ β dom πΌ) |
26 | 4, 5, 6, 7 | diaeldm 39502 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β (π₯ β dom πΌ β (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π))) |
27 | 26 | ad2antrr 725 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (π₯ β dom πΌ β (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π))) |
28 | 25, 27 | mpbid 231 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π)) |
29 | 28 | simpld 496 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π₯ β (BaseβπΎ)) |
30 | 4, 6 | lhpbase 38464 |
. . . . . . 7
β’ (π β π» β π β (BaseβπΎ)) |
31 | 30 | ad3antlr 730 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π β (BaseβπΎ)) |
32 | 2 | ad3antrrr 729 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β πΎ β CLat) |
33 | 13 | adantr 482 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π β (BaseβπΎ)) |
34 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π₯ β π) |
35 | 4, 5, 14 | clatglble 18407 |
. . . . . . 7
β’ ((πΎ β CLat β§ π β (BaseβπΎ) β§ π₯ β π) β (πΊβπ)(leβπΎ)π₯) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (πΊβπ)(leβπΎ)π₯) |
37 | 28 | simprd 497 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β π₯(leβπΎ)π) |
38 | 4, 5, 21, 22, 29, 31, 36, 37 | lattrd 18336 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (πΊβπ)(leβπΎ)π) |
39 | 19, 38 | exlimddv 1939 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (πΊβπ)(leβπΎ)π) |
40 | | eqid 2737 |
. . . . 5
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
41 | | eqid 2737 |
. . . . 5
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
42 | 4, 5, 6, 40, 41, 7 | diaelval 39499 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((πΊβπ) β (BaseβπΎ) β§ (πΊβπ)(leβπΎ)π)) β (π β (πΌβ(πΊβπ)) β (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ)))) |
43 | 1, 16, 39, 42 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (π β (πΌβ(πΊβπ)) β (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ)))) |
44 | | r19.28zv 4459 |
. . . . . 6
β’ (π β β
β
(βπ₯ β π (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)π₯) β (π β ((LTrnβπΎ)βπ) β§ βπ₯ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
45 | 44 | ad2antll 728 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (βπ₯ β π (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)π₯) β (π β ((LTrnβπΎ)βπ) β§ βπ₯ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
46 | | simpll 766 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (πΎ β HL β§ π β π»)) |
47 | 4, 5, 6, 40, 41, 7 | diaelval 39499 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π)) β (π β (πΌβπ₯) β (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
48 | 46, 28, 47 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π₯ β π) β (π β (πΌβπ₯) β (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
49 | 48 | ralbidva 3173 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (βπ₯ β π π β (πΌβπ₯) β βπ₯ β π (π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
50 | 2 | ad3antrrr 729 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π β ((LTrnβπΎ)βπ)) β πΎ β CLat) |
51 | 4, 6, 40, 41 | trlcl 38630 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
52 | 51 | adantlr 714 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
53 | 13 | adantr 482 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π β ((LTrnβπΎ)βπ)) β π β (BaseβπΎ)) |
54 | 4, 5, 14 | clatleglb 18408 |
. . . . . . 7
β’ ((πΎ β CLat β§
(((trLβπΎ)βπ)βπ) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ) β βπ₯ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π₯)) |
55 | 50, 52, 53, 54 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β§ π β ((LTrnβπΎ)βπ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ) β βπ₯ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π₯)) |
56 | 55 | pm5.32da 580 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β ((π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ)) β (π β ((LTrnβπΎ)βπ) β§ βπ₯ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π₯))) |
57 | 45, 49, 56 | 3bitr4rd 312 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β ((π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ)) β βπ₯ β π π β (πΌβπ₯))) |
58 | | vex 3450 |
. . . . 5
β’ π β V |
59 | | eliin 4960 |
. . . . 5
β’ (π β V β (π β β© π₯ β π (πΌβπ₯) β βπ₯ β π π β (πΌβπ₯))) |
60 | 58, 59 | ax-mp 5 |
. . . 4
β’ (π β β© π₯ β π (πΌβπ₯) β βπ₯ β π π β (πΌβπ₯)) |
61 | 57, 60 | bitr4di 289 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β ((π β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)βπ)(leβπΎ)(πΊβπ)) β π β β©
π₯ β π (πΌβπ₯))) |
62 | 43, 61 | bitrd 279 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (π β (πΌβ(πΊβπ)) β π β β©
π₯ β π (πΌβπ₯))) |
63 | 62 | eqrdv 2735 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β
)) β (πΌβ(πΊβπ)) = β©
π₯ β π (πΌβπ₯)) |