Step | Hyp | Ref
| Expression |
1 | | dochvalr.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | eqid 2732 |
. . . 4
β’
((DVecHβπΎ)βπ) = ((DVecHβπΎ)βπ) |
3 | | dochvalr.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
4 | | eqid 2732 |
. . . 4
β’
(Baseβ((DVecHβπΎ)βπ)) = (Baseβ((DVecHβπΎ)βπ)) |
5 | 1, 2, 3, 4 | dihrnss 40137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β (Baseβ((DVecHβπΎ)βπ))) |
6 | | eqid 2732 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | | eqid 2732 |
. . . 4
β’
(glbβπΎ) =
(glbβπΎ) |
8 | | dochvalr.o |
. . . 4
β’ β₯ =
(ocβπΎ) |
9 | | dochvalr.n |
. . . 4
β’ π = ((ocHβπΎ)βπ) |
10 | 6, 7, 8, 1, 3, 2, 4, 9 | dochval 40210 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (Baseβ((DVecHβπΎ)βπ))) β (πβπ) = (πΌβ( β₯
β((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})))) |
11 | 5, 10 | syldan 591 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πβπ) = (πΌβ( β₯
β((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})))) |
12 | | eqid 2732 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
13 | | hllat 38221 |
. . . . . 6
β’ (πΎ β HL β πΎ β Lat) |
14 | 13 | ad2antrr 724 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β πΎ β Lat) |
15 | | hlclat 38216 |
. . . . . . 7
β’ (πΎ β HL β πΎ β CLat) |
16 | 15 | ad2antrr 724 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β πΎ β CLat) |
17 | | ssrab2 4076 |
. . . . . 6
β’ {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (BaseβπΎ) |
18 | 6, 7 | clatglbcl 18454 |
. . . . . 6
β’ ((πΎ β CLat β§ {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (BaseβπΎ)) β ((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) β (BaseβπΎ)) |
19 | 16, 17, 18 | sylancl 586 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) β (BaseβπΎ)) |
20 | 6, 1, 3 | dihcnvcl 40130 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β (BaseβπΎ)) |
21 | 17 | a1i 11 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (BaseβπΎ)) |
22 | | ssid 4003 |
. . . . . . . 8
β’ π β π |
23 | 1, 3 | dihcnvid2 40132 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) |
24 | 22, 23 | sseqtrrid 4034 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β (πΌβ(β‘πΌβπ))) |
25 | | fveq2 6888 |
. . . . . . . . 9
β’ (π¦ = (β‘πΌβπ) β (πΌβπ¦) = (πΌβ(β‘πΌβπ))) |
26 | 25 | sseq2d 4013 |
. . . . . . . 8
β’ (π¦ = (β‘πΌβπ) β (π β (πΌβπ¦) β π β (πΌβ(β‘πΌβπ)))) |
27 | 26 | elrab 3682 |
. . . . . . 7
β’ ((β‘πΌβπ) β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β ((β‘πΌβπ) β (BaseβπΎ) β§ π β (πΌβ(β‘πΌβπ)))) |
28 | 20, 24, 27 | sylanbrc 583 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) |
29 | 6, 12, 7 | clatglble 18466 |
. . . . . 6
β’ ((πΎ β CLat β§ {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (BaseβπΎ) β§ (β‘πΌβπ) β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) β ((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})(leβπΎ)(β‘πΌβπ)) |
30 | 16, 21, 28, 29 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})(leβπΎ)(β‘πΌβπ)) |
31 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π¦ = π§ β (πΌβπ¦) = (πΌβπ§)) |
32 | 31 | sseq2d 4013 |
. . . . . . . . 9
β’ (π¦ = π§ β (π β (πΌβπ¦) β π β (πΌβπ§))) |
33 | 32 | elrab 3682 |
. . . . . . . 8
β’ (π§ β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (π§ β (BaseβπΎ) β§ π β (πΌβπ§))) |
34 | 23 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β (πΌβ(β‘πΌβπ)) = π) |
35 | 34 | sseq1d 4012 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β ((πΌβ(β‘πΌβπ)) β (πΌβπ§) β π β (πΌβπ§))) |
36 | | simpll 765 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β (πΎ β HL β§ π β π»)) |
37 | 20 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β (β‘πΌβπ) β (BaseβπΎ)) |
38 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β π§ β (BaseβπΎ)) |
39 | 6, 12, 1, 3 | dihord 40123 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (β‘πΌβπ) β (BaseβπΎ) β§ π§ β (BaseβπΎ)) β ((πΌβ(β‘πΌβπ)) β (πΌβπ§) β (β‘πΌβπ)(leβπΎ)π§)) |
40 | 36, 37, 38, 39 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β ((πΌβ(β‘πΌβπ)) β (πΌβπ§) β (β‘πΌβπ)(leβπΎ)π§)) |
41 | 35, 40 | bitr3d 280 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β (π β (πΌβπ§) β (β‘πΌβπ)(leβπΎ)π§)) |
42 | 41 | biimpd 228 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β ran πΌ) β§ π§ β (BaseβπΎ)) β (π β (πΌβπ§) β (β‘πΌβπ)(leβπΎ)π§)) |
43 | 42 | expimpd 454 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ((π§ β (BaseβπΎ) β§ π β (πΌβπ§)) β (β‘πΌβπ)(leβπΎ)π§)) |
44 | 33, 43 | biimtrid 241 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (π§ β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (β‘πΌβπ)(leβπΎ)π§)) |
45 | 44 | ralrimiv 3145 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β βπ§ β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} (β‘πΌβπ)(leβπΎ)π§) |
46 | 6, 12, 7 | clatleglb 18467 |
. . . . . . 7
β’ ((πΎ β CLat β§ (β‘πΌβπ) β (BaseβπΎ) β§ {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} β (BaseβπΎ)) β ((β‘πΌβπ)(leβπΎ)((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) β βπ§ β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} (β‘πΌβπ)(leβπΎ)π§)) |
47 | 16, 20, 21, 46 | syl3anc 1371 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ((β‘πΌβπ)(leβπΎ)((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) β βπ§ β {π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)} (β‘πΌβπ)(leβπΎ)π§)) |
48 | 45, 47 | mpbird 256 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ)(leβπΎ)((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})) |
49 | 6, 12, 14, 19, 20, 30, 48 | latasymd 18394 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}) = (β‘πΌβπ)) |
50 | 49 | fveq2d 6892 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ( β₯
β((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)})) = ( β₯ β(β‘πΌβπ))) |
51 | 50 | fveq2d 6892 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ( β₯
β((glbβπΎ)β{π¦ β (BaseβπΎ) β£ π β (πΌβπ¦)}))) = (πΌβ( β₯ β(β‘πΌβπ)))) |
52 | 11, 51 | eqtrd 2772 |
1
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πβπ) = (πΌβ( β₯ β(β‘πΌβπ)))) |