Step | Hyp | Ref
| Expression |
1 | | odulub.l |
. 2
β’ πΏ = (glbβπ) |
2 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
3 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
4 | 2, 3 | brcnv 5842 |
. . . . . . . . . 10
β’ (πβ‘(leβπ)π β π(leβπ)π) |
5 | 4 | ralbii 3093 |
. . . . . . . . 9
β’
(βπ β
π πβ‘(leβπ)π β βπ β π π(leβπ)π) |
6 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
7 | 2, 6 | brcnv 5842 |
. . . . . . . . . . . 12
β’ (πβ‘(leβπ)π β π(leβπ)π) |
8 | 7 | ralbii 3093 |
. . . . . . . . . . 11
β’
(βπ β
π πβ‘(leβπ)π β βπ β π π(leβπ)π) |
9 | 3, 6 | brcnv 5842 |
. . . . . . . . . . 11
β’ (πβ‘(leβπ)π β π(leβπ)π) |
10 | 8, 9 | imbi12i 351 |
. . . . . . . . . 10
β’
((βπ β
π πβ‘(leβπ)π β πβ‘(leβπ)π) β (βπ β π π(leβπ)π β π(leβπ)π)) |
11 | 10 | ralbii 3093 |
. . . . . . . . 9
β’
(βπ β
(Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π) β βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)) |
12 | 5, 11 | anbi12i 628 |
. . . . . . . 8
β’
((βπ β
π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)) β (βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))) |
13 | 12 | a1i 11 |
. . . . . . 7
β’ (π β (Baseβπ) β ((βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)) β (βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)))) |
14 | 13 | riotabiia 7338 |
. . . . . 6
β’
(β©π
β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))) = (β©π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))) |
15 | 14 | mpteq2i 5214 |
. . . . 5
β’ (π β π«
(Baseβπ) β¦
(β©π β
(Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)))) = (π β π« (Baseβπ) β¦ (β©π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)))) |
16 | 12 | reubii 3361 |
. . . . . 6
β’
(β!π β
(Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)) β β!π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))) |
17 | 16 | abbii 2803 |
. . . . 5
β’ {π β£ β!π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))} = {π β£ β!π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))} |
18 | 15, 17 | reseq12i 5939 |
. . . 4
β’ ((π β π«
(Baseβπ) β¦
(β©π β
(Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))}) = ((π β π« (Baseβπ) β¦ (β©π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))}) |
19 | 18 | eqcomi 2742 |
. . 3
β’ ((π β π«
(Baseβπ) β¦
(β©π β
(Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))}) = ((π β π« (Baseβπ) β¦ (β©π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))}) |
20 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
21 | | eqid 2733 |
. . . 4
β’
(leβπ) =
(leβπ) |
22 | | eqid 2733 |
. . . 4
β’
(glbβπ) =
(glbβπ) |
23 | | biid 261 |
. . . 4
β’
((βπ β
π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)) β (βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))) |
24 | | id 22 |
. . . 4
β’ (π β π β π β π) |
25 | 20, 21, 22, 23, 24 | glbfval 18260 |
. . 3
β’ (π β π β (glbβπ) = ((π β π« (Baseβπ) β¦ (β©π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π π(leβπ)π β§ βπ β (Baseβπ)(βπ β π π(leβπ)π β π(leβπ)π))})) |
26 | | oduglb.d |
. . . . 5
β’ π· = (ODualβπ) |
27 | 26 | fvexi 6860 |
. . . 4
β’ π· β V |
28 | 26, 20 | odubas 18188 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ·) |
29 | 26, 21 | oduleval 18186 |
. . . . 5
β’ β‘(leβπ) = (leβπ·) |
30 | | eqid 2733 |
. . . . 5
β’
(lubβπ·) =
(lubβπ·) |
31 | | biid 261 |
. . . . 5
β’
((βπ β
π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)) β (βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))) |
32 | | id 22 |
. . . . 5
β’ (π· β V β π· β V) |
33 | 28, 29, 30, 31, 32 | lubfval 18247 |
. . . 4
β’ (π· β V β
(lubβπ·) = ((π β π«
(Baseβπ) β¦
(β©π β
(Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))})) |
34 | 27, 33 | mp1i 13 |
. . 3
β’ (π β π β (lubβπ·) = ((π β π« (Baseβπ) β¦ (β©π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π)))) βΎ {π β£ β!π β (Baseβπ)(βπ β π πβ‘(leβπ)π β§ βπ β (Baseβπ)(βπ β π πβ‘(leβπ)π β πβ‘(leβπ)π))})) |
35 | 19, 25, 34 | 3eqtr4a 2799 |
. 2
β’ (π β π β (glbβπ) = (lubβπ·)) |
36 | 1, 35 | eqtrid 2785 |
1
β’ (π β π β πΏ = (lubβπ·)) |