Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(leβπΎ) =
(leβπΎ) |
3 | 1, 2 | isprs 18191 |
. . . . . . . . . . . . 13
β’ (πΎ β Proset β (πΎ β V β§ βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
4 | 3 | simprbi 498 |
. . . . . . . . . . . 12
β’ (πΎ β Proset β
βπ₯ β
(BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
5 | 4 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ ((πΎ β Proset β§ π₯ β (BaseβπΎ)) β βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
6 | 5 | r19.21bi 3233 |
. . . . . . . . . 10
β’ (((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
7 | 6 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
8 | 7 | simpld 496 |
. . . . . . . 8
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β π₯(leβπΎ)π₯) |
9 | | vex 3448 |
. . . . . . . . 9
β’ π₯ β V |
10 | 9, 9 | brcnv 5839 |
. . . . . . . 8
β’ (π₯β‘(leβπΎ)π₯ β π₯(leβπΎ)π₯) |
11 | 8, 10 | sylibr 233 |
. . . . . . 7
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β π₯β‘(leβπΎ)π₯) |
12 | 1, 2 | isprs 18191 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β Proset β (πΎ β V β§ βπ§ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ₯ β (BaseβπΎ)(π§(leβπΎ)π§ β§ ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯)))) |
13 | 12 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β Proset β
βπ§ β
(BaseβπΎ)βπ¦ β (BaseβπΎ)βπ₯ β (BaseβπΎ)(π§(leβπΎ)π§ β§ ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
14 | 13 | r19.21bi 3233 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Proset β§ π§ β (BaseβπΎ)) β βπ¦ β (BaseβπΎ)βπ₯ β (BaseβπΎ)(π§(leβπΎ)π§ β§ ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
15 | 14 | r19.21bi 3233 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β Proset β§ π§ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β βπ₯ β (BaseβπΎ)(π§(leβπΎ)π§ β§ ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
16 | 15 | r19.21bi 3233 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β Proset β§ π§ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π₯ β (BaseβπΎ)) β (π§(leβπΎ)π§ β§ ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
17 | 16 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((((πΎ β Proset β§ π§ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π₯ β (BaseβπΎ)) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯)) |
18 | 17 | an32s 651 |
. . . . . . . . . . . 12
β’ ((((πΎ β Proset β§ π§ β (BaseβπΎ)) β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯)) |
19 | 18 | ex 414 |
. . . . . . . . . . 11
β’ (((πΎ β Proset β§ π§ β (BaseβπΎ)) β§ π₯ β (BaseβπΎ)) β (π¦ β (BaseβπΎ) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
20 | 19 | an32s 651 |
. . . . . . . . . 10
β’ (((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β (π¦ β (BaseβπΎ) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯))) |
21 | 20 | imp 408 |
. . . . . . . . 9
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯)) |
22 | 21 | an32s 651 |
. . . . . . . 8
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β ((π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯) β π§(leβπΎ)π₯)) |
23 | | vex 3448 |
. . . . . . . . . 10
β’ π¦ β V |
24 | 9, 23 | brcnv 5839 |
. . . . . . . . 9
β’ (π₯β‘(leβπΎ)π¦ β π¦(leβπΎ)π₯) |
25 | | vex 3448 |
. . . . . . . . . 10
β’ π§ β V |
26 | 23, 25 | brcnv 5839 |
. . . . . . . . 9
β’ (π¦β‘(leβπΎ)π§ β π§(leβπΎ)π¦) |
27 | 24, 26 | anbi12ci 629 |
. . . . . . . 8
β’ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β (π§(leβπΎ)π¦ β§ π¦(leβπΎ)π₯)) |
28 | 9, 25 | brcnv 5839 |
. . . . . . . 8
β’ (π₯β‘(leβπΎ)π§ β π§(leβπΎ)π₯) |
29 | 22, 27, 28 | 3imtr4g 296 |
. . . . . . 7
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§)) |
30 | 11, 29 | jca 513 |
. . . . . 6
β’ ((((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β (π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§))) |
31 | 30 | ralrimiva 3140 |
. . . . 5
β’ (((πΎ β Proset β§ π₯ β (BaseβπΎ)) β§ π¦ β (BaseβπΎ)) β βπ§ β (BaseβπΎ)(π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§))) |
32 | 31 | ralrimiva 3140 |
. . . 4
β’ ((πΎ β Proset β§ π₯ β (BaseβπΎ)) β βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§))) |
33 | 32 | ralrimiva 3140 |
. . 3
β’ (πΎ β Proset β
βπ₯ β
(BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§))) |
34 | | oduprs.d |
. . . 4
β’ π· = (ODualβπΎ) |
35 | 34 | fvexi 6857 |
. . 3
β’ π· β V |
36 | 33, 35 | jctil 521 |
. 2
β’ (πΎ β Proset β (π· β V β§ βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§)))) |
37 | 34, 1 | odubas 18185 |
. . 3
β’
(BaseβπΎ) =
(Baseβπ·) |
38 | 34, 2 | oduleval 18183 |
. . 3
β’ β‘(leβπΎ) = (leβπ·) |
39 | 37, 38 | isprs 18191 |
. 2
β’ (π· β Proset β (π· β V β§ βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯β‘(leβπΎ)π₯ β§ ((π₯β‘(leβπΎ)π¦ β§ π¦β‘(leβπΎ)π§) β π₯β‘(leβπΎ)π§)))) |
40 | 36, 39 | sylibr 233 |
1
β’ (πΎ β Proset β π· β Proset
) |