Step | Hyp | Ref
| Expression |
1 | | dih1.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | dih1.i |
. . 3
β’ πΌ = ((DIsoHβπΎ)βπ) |
3 | 1, 2 | dihvalrel 39628 |
. 2
β’ ((πΎ β HL β§ π β π») β Rel (πΌβ 1 )) |
4 | | relxp 5649 |
. . 3
β’ Rel
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) |
5 | | eqid 2738 |
. . . . 5
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
6 | | eqid 2738 |
. . . . 5
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
7 | | dih1.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
8 | | dih1.v |
. . . . 5
β’ π = (Baseβπ) |
9 | 1, 5, 6, 7, 8 | dvhvbase 39436 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π = (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ))) |
10 | 9 | releqd 5731 |
. . 3
β’ ((πΎ β HL β§ π β π») β (Rel π β Rel (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)))) |
11 | 4, 10 | mpbiri 258 |
. 2
β’ ((πΎ β HL β§ π β π») β Rel π) |
12 | | id 22 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
13 | | hlop 37710 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
14 | 13 | ad2antrr 725 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β πΎ β OP) |
15 | | simpl 484 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (πΎ β HL β§ π β π»)) |
16 | | simprl 770 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β π β ((LTrnβπΎ)βπ)) |
17 | | simprr 772 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β π β ((TEndoβπΎ)βπ)) |
18 | | eqid 2738 |
. . . . . . . . . . . . . 14
β’
(leβπΎ) =
(leβπΎ) |
19 | | eqid 2738 |
. . . . . . . . . . . . . 14
β’
(ocβπΎ) =
(ocβπΎ) |
20 | | eqid 2738 |
. . . . . . . . . . . . . 14
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
21 | 18, 19, 20, 1 | lhpocnel 38367 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ) β (AtomsβπΎ) β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
22 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (((ocβπΎ)βπ) β (AtomsβπΎ) β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
23 | | eqid 2738 |
. . . . . . . . . . . . 13
β’
(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) = (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) |
24 | 18, 20, 1, 5, 23 | ltrniotacl 38928 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (((ocβπΎ)βπ) β (AtomsβπΎ) β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π) β§ (((ocβπΎ)βπ) β (AtomsβπΎ) β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) β ((LTrnβπΎ)βπ)) |
25 | 15, 22, 22, 24 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) β ((LTrnβπΎ)βπ)) |
26 | 1, 5, 6 | tendocl 39116 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π β ((TEndoβπΎ)βπ) β§ (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) β ((LTrnβπΎ)βπ)) β (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) |
27 | 15, 17, 25, 26 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) |
28 | 1, 5 | ltrncnv 38495 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) |
29 | 27, 28 | syldan 592 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) |
30 | 1, 5 | ltrnco 39068 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ) β§ β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))) β ((LTrnβπΎ)βπ)) β (π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))) β ((LTrnβπΎ)βπ)) |
31 | 15, 16, 29, 30 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))) β ((LTrnβπΎ)βπ)) |
32 | | eqid 2738 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
33 | | eqid 2738 |
. . . . . . . . 9
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
34 | 32, 1, 5, 33 | trlcl 38513 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))))) β (BaseβπΎ)) |
35 | 31, 34 | syldan 592 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))))) β (BaseβπΎ)) |
36 | | dih1.m |
. . . . . . . 8
β’ 1 =
(1.βπΎ) |
37 | 32, 18, 36 | ople1 37539 |
. . . . . . 7
β’ ((πΎ β OP β§
(((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ))))) β (BaseβπΎ)) β (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 ) |
38 | 14, 35, 37 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) β (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 ) |
39 | 38 | ex 414 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)) β (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 )) |
40 | 39 | pm4.71d 563 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)) β ((π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)) β§ (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 ))) |
41 | 9 | eleq2d 2824 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (β¨π, π β© β π β β¨π, π β© β (((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)))) |
42 | | opelxp 5667 |
. . . . 5
β’
(β¨π, π β© β
(((LTrnβπΎ)βπ) Γ ((TEndoβπΎ)βπ)) β (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ))) |
43 | 41, 42 | bitrdi 287 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (β¨π, π β© β π β (π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)))) |
44 | 13 | adantr 482 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β πΎ β OP) |
45 | 32, 36 | op1cl 37533 |
. . . . . 6
β’ (πΎ β OP β 1 β
(BaseβπΎ)) |
46 | 44, 45 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β 1 β (BaseβπΎ)) |
47 | | hlpos 37714 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Poset) |
48 | 47 | adantr 482 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β πΎ β Poset) |
49 | 32, 1 | lhpbase 38347 |
. . . . . . 7
β’ (π β π» β π β (BaseβπΎ)) |
50 | 49 | adantl 483 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β π β (BaseβπΎ)) |
51 | | eqid 2738 |
. . . . . . 7
β’ ( β
βπΎ) = ( β
βπΎ) |
52 | 36, 51, 1 | lhp1cvr 38348 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β π( β βπΎ) 1 ) |
53 | 32, 18, 51 | cvrnle 37628 |
. . . . . 6
β’ (((πΎ β Poset β§ π β (BaseβπΎ) β§ 1 β (BaseβπΎ)) β§ π( β βπΎ) 1 ) β Β¬ 1
(leβπΎ)π) |
54 | 48, 50, 46, 52, 53 | syl31anc 1374 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β Β¬ 1 (leβπΎ)π) |
55 | | hlol 37709 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OL) |
56 | | eqid 2738 |
. . . . . . . . 9
β’
(meetβπΎ) =
(meetβπΎ) |
57 | 32, 56, 36 | olm12 37576 |
. . . . . . . 8
β’ ((πΎ β OL β§ π β (BaseβπΎ)) β ( 1 (meetβπΎ)π) = π) |
58 | 55, 49, 57 | syl2an 597 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ( 1 (meetβπΎ)π) = π) |
59 | 58 | oveq2d 7366 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ)(joinβπΎ)( 1 (meetβπΎ)π)) = (((ocβπΎ)βπ)(joinβπΎ)π)) |
60 | | hllat 37711 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β Lat) |
61 | 60 | adantr 482 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β πΎ β Lat) |
62 | 32, 19 | opoccl 37542 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
63 | 13, 49, 62 | syl2an 597 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ((ocβπΎ)βπ) β (BaseβπΎ)) |
64 | | eqid 2738 |
. . . . . . . 8
β’
(joinβπΎ) =
(joinβπΎ) |
65 | 32, 64 | latjcom 18271 |
. . . . . . 7
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((ocβπΎ)βπ)(joinβπΎ)π) = (π(joinβπΎ)((ocβπΎ)βπ))) |
66 | 61, 63, 50, 65 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ)(joinβπΎ)π) = (π(joinβπΎ)((ocβπΎ)βπ))) |
67 | 32, 19, 64, 36 | opexmid 37555 |
. . . . . . 7
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β (π(joinβπΎ)((ocβπΎ)βπ)) = 1 ) |
68 | 13, 49, 67 | syl2an 597 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (π(joinβπΎ)((ocβπΎ)βπ)) = 1 ) |
69 | 59, 66, 68 | 3eqtrd 2782 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ)(joinβπΎ)( 1 (meetβπΎ)π)) = 1 ) |
70 | | eqid 2738 |
. . . . . 6
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
71 | | vex 3448 |
. . . . . 6
β’ π β V |
72 | | vex 3448 |
. . . . . 6
β’ π β V |
73 | 32, 18, 64, 56, 20, 1, 70, 5, 33, 6, 2, 23, 71, 72 | dihopelvalc 39598 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( 1 β (BaseβπΎ) β§ Β¬ 1 (leβπΎ)π) β§ ((((ocβπΎ)βπ) β (AtomsβπΎ) β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)( 1 (meetβπΎ)π)) = 1 )) β (β¨π, π β© β (πΌβ 1 ) β ((π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)) β§ (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 ))) |
74 | 12, 46, 54, 21, 69, 73 | syl122anc 1380 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (β¨π, π β© β (πΌβ 1 ) β ((π β ((LTrnβπΎ)βπ) β§ π β ((TEndoβπΎ)βπ)) β§ (((trLβπΎ)βπ)β(π β β‘(π β(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)))))(leβπΎ) 1 ))) |
75 | 40, 43, 74 | 3bitr4rd 312 |
. . 3
β’ ((πΎ β HL β§ π β π») β (β¨π, π β© β (πΌβ 1 ) β β¨π, π β© β π)) |
76 | 75 | eqrelrdv2 5748 |
. 2
β’ (((Rel
(πΌβ 1 ) β§ Rel
π) β§ (πΎ β HL β§ π β π»)) β (πΌβ 1 ) = π) |
77 | 3, 11, 12, 76 | syl21anc 837 |
1
β’ ((πΎ β HL β§ π β π») β (πΌβ 1 ) = π) |