Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . 4
β’
(meetβπΎ) =
(meetβπΎ) |
2 | | dihoml4c.h |
. . . 4
β’ π» = (LHypβπΎ) |
3 | | dihoml4c.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
4 | | dihoml4c.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
5 | | inss1 4228 |
. . . . . 6
β’ (( β₯
βπ) β© π) β ( β₯ βπ) |
6 | | dihoml4c.x |
. . . . . . . 8
β’ (π β π β ran πΌ) |
7 | | eqid 2732 |
. . . . . . . . 9
β’
((DVecHβπΎ)βπ) = ((DVecHβπΎ)βπ) |
8 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβ((DVecHβπΎ)βπ)) = (Baseβ((DVecHβπΎ)βπ)) |
9 | 2, 7, 3, 8 | dihrnss 40452 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β (Baseβ((DVecHβπΎ)βπ))) |
10 | 4, 6, 9 | syl2anc 584 |
. . . . . . 7
β’ (π β π β (Baseβ((DVecHβπΎ)βπ))) |
11 | | dihoml4c.o |
. . . . . . . 8
β’ β₯ =
((ocHβπΎ)βπ) |
12 | 2, 7, 8, 11 | dochssv 40529 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β (Baseβ((DVecHβπΎ)βπ))) β ( β₯ βπ) β
(Baseβ((DVecHβπΎ)βπ))) |
13 | 4, 10, 12 | syl2anc 584 |
. . . . . 6
β’ (π β ( β₯ βπ) β
(Baseβ((DVecHβπΎ)βπ))) |
14 | 5, 13 | sstrid 3993 |
. . . . 5
β’ (π β (( β₯ βπ) β© π) β (Baseβ((DVecHβπΎ)βπ))) |
15 | 2, 3, 7, 8, 11 | dochcl 40527 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (( β₯ βπ) β© π) β (Baseβ((DVecHβπΎ)βπ))) β ( β₯ β(( β₯
βπ) β© π)) β ran πΌ) |
16 | 4, 14, 15 | syl2anc 584 |
. . . 4
β’ (π β ( β₯ β(( β₯
βπ) β© π)) β ran πΌ) |
17 | | dihoml4c.y |
. . . 4
β’ (π β π β ran πΌ) |
18 | 1, 2, 3, 4, 16, 17 | dihmeet2 40520 |
. . 3
β’ (π β (β‘πΌβ(( β₯ β(( β₯
βπ) β© π)) β© π)) = ((β‘πΌβ( β₯ β(( β₯
βπ) β© π)))(meetβπΎ)(β‘πΌβπ))) |
19 | | eqid 2732 |
. . . . . 6
β’
(ocβπΎ) =
(ocβπΎ) |
20 | 2, 3, 7, 8, 11 | dochcl 40527 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β (Baseβ((DVecHβπΎ)βπ))) β ( β₯ βπ) β ran πΌ) |
21 | 4, 10, 20 | syl2anc 584 |
. . . . . . 7
β’ (π β ( β₯ βπ) β ran πΌ) |
22 | 2, 3 | dihmeetcl 40519 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (( β₯ βπ) β ran πΌ β§ π β ran πΌ)) β (( β₯ βπ) β© π) β ran πΌ) |
23 | 4, 21, 17, 22 | syl12anc 835 |
. . . . . 6
β’ (π β (( β₯ βπ) β© π) β ran πΌ) |
24 | 19, 2, 3, 11, 4, 23 | dochvalr3 40537 |
. . . . 5
β’ (π β ((ocβπΎ)β(β‘πΌβ(( β₯ βπ) β© π))) = (β‘πΌβ( β₯ β(( β₯
βπ) β© π)))) |
25 | 1, 2, 3, 4, 21, 17 | dihmeet2 40520 |
. . . . . . 7
β’ (π β (β‘πΌβ(( β₯ βπ) β© π)) = ((β‘πΌβ( β₯ βπ))(meetβπΎ)(β‘πΌβπ))) |
26 | 19, 2, 3, 11, 4, 6 | dochvalr3 40537 |
. . . . . . . 8
β’ (π β ((ocβπΎ)β(β‘πΌβπ)) = (β‘πΌβ( β₯ βπ))) |
27 | 26 | oveq1d 7426 |
. . . . . . 7
β’ (π β (((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)) = ((β‘πΌβ( β₯ βπ))(meetβπΎ)(β‘πΌβπ))) |
28 | 25, 27 | eqtr4d 2775 |
. . . . . 6
β’ (π β (β‘πΌβ(( β₯ βπ) β© π)) = (((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ))) |
29 | 28 | fveq2d 6895 |
. . . . 5
β’ (π β ((ocβπΎ)β(β‘πΌβ(( β₯ βπ) β© π))) = ((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))) |
30 | 24, 29 | eqtr3d 2774 |
. . . 4
β’ (π β (β‘πΌβ( β₯ β(( β₯
βπ) β© π))) = ((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))) |
31 | 30 | oveq1d 7426 |
. . 3
β’ (π β ((β‘πΌβ( β₯ β(( β₯
βπ) β© π)))(meetβπΎ)(β‘πΌβπ)) = (((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))(meetβπΎ)(β‘πΌβπ))) |
32 | | dihoml4c.l |
. . . . 5
β’ (π β π β π) |
33 | | eqid 2732 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
34 | 33, 2, 3, 4, 6, 17 | dihcnvord 40448 |
. . . . 5
β’ (π β ((β‘πΌβπ)(leβπΎ)(β‘πΌβπ) β π β π)) |
35 | 32, 34 | mpbird 256 |
. . . 4
β’ (π β (β‘πΌβπ)(leβπΎ)(β‘πΌβπ)) |
36 | 4 | simpld 495 |
. . . . . 6
β’ (π β πΎ β HL) |
37 | | hloml 38530 |
. . . . . 6
β’ (πΎ β HL β πΎ β OML) |
38 | 36, 37 | syl 17 |
. . . . 5
β’ (π β πΎ β OML) |
39 | | eqid 2732 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
40 | 39, 2, 3 | dihcnvcl 40445 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β (BaseβπΎ)) |
41 | 4, 6, 40 | syl2anc 584 |
. . . . 5
β’ (π β (β‘πΌβπ) β (BaseβπΎ)) |
42 | 39, 2, 3 | dihcnvcl 40445 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β (BaseβπΎ)) |
43 | 4, 17, 42 | syl2anc 584 |
. . . . 5
β’ (π β (β‘πΌβπ) β (BaseβπΎ)) |
44 | 39, 33, 1, 19 | omllaw4 38419 |
. . . . 5
β’ ((πΎ β OML β§ (β‘πΌβπ) β (BaseβπΎ) β§ (β‘πΌβπ) β (BaseβπΎ)) β ((β‘πΌβπ)(leβπΎ)(β‘πΌβπ) β (((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))(meetβπΎ)(β‘πΌβπ)) = (β‘πΌβπ))) |
45 | 38, 41, 43, 44 | syl3anc 1371 |
. . . 4
β’ (π β ((β‘πΌβπ)(leβπΎ)(β‘πΌβπ) β (((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))(meetβπΎ)(β‘πΌβπ)) = (β‘πΌβπ))) |
46 | 35, 45 | mpd 15 |
. . 3
β’ (π β (((ocβπΎ)β(((ocβπΎ)β(β‘πΌβπ))(meetβπΎ)(β‘πΌβπ)))(meetβπΎ)(β‘πΌβπ)) = (β‘πΌβπ)) |
47 | 18, 31, 46 | 3eqtrd 2776 |
. 2
β’ (π β (β‘πΌβ(( β₯ β(( β₯
βπ) β© π)) β© π)) = (β‘πΌβπ)) |
48 | 2, 3 | dihmeetcl 40519 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (( β₯ β(( β₯
βπ) β© π)) β ran πΌ β§ π β ran πΌ)) β (( β₯ β(( β₯
βπ) β© π)) β© π) β ran πΌ) |
49 | 4, 16, 17, 48 | syl12anc 835 |
. . 3
β’ (π β (( β₯ β(( β₯
βπ) β© π)) β© π) β ran πΌ) |
50 | 2, 3, 4, 49, 6 | dihcnv11 40449 |
. 2
β’ (π β ((β‘πΌβ(( β₯ β(( β₯
βπ) β© π)) β© π)) = (β‘πΌβπ) β (( β₯ β(( β₯
βπ) β© π)) β© π) = π)) |
51 | 47, 50 | mpbid 231 |
1
β’ (π β (( β₯ β(( β₯
βπ) β© π)) β© π) = π) |