Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2737 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
3 | | glb0.g |
. . 3
β’ πΊ = (glbβπΎ) |
4 | | biid 261 |
. . 3
β’
((βπ¦ β
β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯)) β (βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
5 | | id 22 |
. . 3
β’ (πΎ β OP β πΎ β OP) |
6 | | 0ss 4357 |
. . . 4
β’ β
β (BaseβπΎ) |
7 | 6 | a1i 11 |
. . 3
β’ (πΎ β OP β β
β (BaseβπΎ)) |
8 | 1, 2, 3, 4, 5, 7 | glbval 18259 |
. 2
β’ (πΎ β OP β (πΊββ
) =
(β©π₯ β
(BaseβπΎ)(βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯)))) |
9 | | glb0.u |
. . . 4
β’ 1 =
(1.βπΎ) |
10 | 1, 9 | op1cl 37650 |
. . 3
β’ (πΎ β OP β 1 β
(BaseβπΎ)) |
11 | | ral0 4471 |
. . . . . . 7
β’
βπ¦ β
β
π§(leβπΎ)π¦ |
12 | 11 | a1bi 363 |
. . . . . 6
β’ (π§(leβπΎ)π₯ β (βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯)) |
13 | 12 | ralbii 3097 |
. . . . 5
β’
(βπ§ β
(BaseβπΎ)π§(leβπΎ)π₯ β βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯)) |
14 | | ral0 4471 |
. . . . . 6
β’
βπ¦ β
β
π₯(leβπΎ)π¦ |
15 | 14 | biantrur 532 |
. . . . 5
β’
(βπ§ β
(BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯) β (βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
16 | 13, 15 | bitri 275 |
. . . 4
β’
(βπ§ β
(BaseβπΎ)π§(leβπΎ)π₯ β (βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
17 | 10 | adantr 482 |
. . . . . . 7
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β 1 β (BaseβπΎ)) |
18 | | breq1 5109 |
. . . . . . . 8
β’ (π§ = 1 β (π§(leβπΎ)π₯ β 1 (leβπΎ)π₯)) |
19 | 18 | rspcv 3578 |
. . . . . . 7
β’ ( 1 β
(BaseβπΎ) β
(βπ§ β
(BaseβπΎ)π§(leβπΎ)π₯ β 1 (leβπΎ)π₯)) |
20 | 17, 19 | syl 17 |
. . . . . 6
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (βπ§ β (BaseβπΎ)π§(leβπΎ)π₯ β 1 (leβπΎ)π₯)) |
21 | 1, 2, 9 | op1le 37657 |
. . . . . 6
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β ( 1 (leβπΎ)π₯ β π₯ = 1 )) |
22 | 20, 21 | sylibd 238 |
. . . . 5
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (βπ§ β (BaseβπΎ)π§(leβπΎ)π₯ β π₯ = 1 )) |
23 | 1, 2, 9 | ople1 37656 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π§ β (BaseβπΎ)) β π§(leβπΎ) 1 ) |
24 | 23 | adantlr 714 |
. . . . . . . . 9
β’ (((πΎ β OP β§ π₯ β (BaseβπΎ)) β§ π§ β (BaseβπΎ)) β π§(leβπΎ) 1 ) |
25 | 24 | ex 414 |
. . . . . . . 8
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (π§ β (BaseβπΎ) β π§(leβπΎ) 1 )) |
26 | | breq2 5110 |
. . . . . . . . 9
β’ (π₯ = 1 β (π§(leβπΎ)π₯ β π§(leβπΎ) 1 )) |
27 | 26 | biimprcd 250 |
. . . . . . . 8
β’ (π§(leβπΎ) 1 β (π₯ = 1 β π§(leβπΎ)π₯)) |
28 | 25, 27 | syl6 35 |
. . . . . . 7
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (π§ β (BaseβπΎ) β (π₯ = 1 β π§(leβπΎ)π₯))) |
29 | 28 | com23 86 |
. . . . . 6
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (π₯ = 1 β (π§ β (BaseβπΎ) β π§(leβπΎ)π₯))) |
30 | 29 | ralrimdv 3150 |
. . . . 5
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (π₯ = 1 β βπ§ β (BaseβπΎ)π§(leβπΎ)π₯)) |
31 | 22, 30 | impbid 211 |
. . . 4
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β (βπ§ β (BaseβπΎ)π§(leβπΎ)π₯ β π₯ = 1 )) |
32 | 16, 31 | bitr3id 285 |
. . 3
β’ ((πΎ β OP β§ π₯ β (BaseβπΎ)) β ((βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯)) β π₯ = 1 )) |
33 | 10, 32 | riota5 7344 |
. 2
β’ (πΎ β OP β
(β©π₯ β
(BaseβπΎ)(βπ¦ β β
π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β β
π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) = 1 ) |
34 | 8, 33 | eqtrd 2777 |
1
β’ (πΎ β OP β (πΊββ
) = 1
) |