Step | Hyp | Ref
| Expression |
1 | | df-mgc 31890 |
. . 3
β’ MGalConn
= (π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))}) |
2 | 1 | a1i 11 |
. 2
β’ ((π β π β§ π β π) β MGalConn = (π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))})) |
3 | | fvexd 6858 |
. . 3
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β (Baseβπ£) β V) |
4 | | simprl 770 |
. . . . 5
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β π£ = π) |
5 | 4 | fveq2d 6847 |
. . . 4
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β (Baseβπ£) = (Baseβπ)) |
6 | | mgcoval.1 |
. . . 4
β’ π΄ = (Baseβπ) |
7 | 5, 6 | eqtr4di 2791 |
. . 3
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β (Baseβπ£) = π΄) |
8 | | fvexd 6858 |
. . . 4
β’ ((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β (Baseβπ€) β V) |
9 | | simplrr 777 |
. . . . . 6
β’ ((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β π€ = π) |
10 | 9 | fveq2d 6847 |
. . . . 5
β’ ((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β (Baseβπ€) = (Baseβπ)) |
11 | | mgcoval.2 |
. . . . 5
β’ π΅ = (Baseβπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . 4
β’ ((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β (Baseβπ€) = π΅) |
13 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β π = π΅) |
14 | | simplr 768 |
. . . . . . . . 9
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β π = π΄) |
15 | 13, 14 | oveq12d 7376 |
. . . . . . . 8
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (π βm π) = (π΅ βm π΄)) |
16 | 15 | eleq2d 2820 |
. . . . . . 7
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (π β (π βm π) β π β (π΅ βm π΄))) |
17 | 14, 13 | oveq12d 7376 |
. . . . . . . 8
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (π βm π) = (π΄ βm π΅)) |
18 | 17 | eleq2d 2820 |
. . . . . . 7
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (π β (π βm π) β π β (π΄ βm π΅))) |
19 | 16, 18 | anbi12d 632 |
. . . . . 6
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β ((π β (π βm π) β§ π β (π βm π)) β (π β (π΅ βm π΄) β§ π β (π΄ βm π΅)))) |
20 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β π€ = π) |
21 | 20 | fveq2d 6847 |
. . . . . . . . . . 11
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (leβπ€) = (leβπ)) |
22 | | mgcoval.4 |
. . . . . . . . . . 11
β’ β² =
(leβπ) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . . 10
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (leβπ€) = β² ) |
24 | 23 | breqd 5117 |
. . . . . . . . 9
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β ((πβπ₯)(leβπ€)π¦ β (πβπ₯) β² π¦)) |
25 | 4 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β π£ = π) |
26 | 25 | fveq2d 6847 |
. . . . . . . . . . 11
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (leβπ£) = (leβπ)) |
27 | | mgcoval.3 |
. . . . . . . . . . 11
β’ β€ =
(leβπ) |
28 | 26, 27 | eqtr4di 2791 |
. . . . . . . . . 10
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (leβπ£) = β€ ) |
29 | 28 | breqd 5117 |
. . . . . . . . 9
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (π₯(leβπ£)(πβπ¦) β π₯ β€ (πβπ¦))) |
30 | 24, 29 | bibi12d 346 |
. . . . . . . 8
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) β ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))) |
31 | 13, 30 | raleqbidv 3318 |
. . . . . . 7
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) β βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))) |
32 | 14, 31 | raleqbidv 3318 |
. . . . . 6
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)) β βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))) |
33 | 19, 32 | anbi12d 632 |
. . . . 5
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β (((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦))) β ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦))))) |
34 | 33 | opabbidv 5172 |
. . . 4
β’
(((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β§ π = π΅) β {β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
35 | 8, 12, 34 | csbied2 3896 |
. . 3
β’ ((((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β§ π = π΄) β β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
36 | 3, 7, 35 | csbied2 3896 |
. 2
β’ (((π β π β§ π β π) β§ (π£ = π β§ π€ = π)) β β¦(Baseβπ£) / πβ¦β¦(Baseβπ€) / πβ¦{β¨π, πβ© β£ ((π β (π βm π) β§ π β (π βm π)) β§ βπ₯ β π βπ¦ β π ((πβπ₯)(leβπ€)π¦ β π₯(leβπ£)(πβπ¦)))} = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |
37 | | simpl 484 |
. . 3
β’ ((π β π β§ π β π) β π β π) |
38 | 37 | elexd 3464 |
. 2
β’ ((π β π β§ π β π) β π β V) |
39 | | simpr 486 |
. . 3
β’ ((π β π β§ π β π) β π β π) |
40 | 39 | elexd 3464 |
. 2
β’ ((π β π β§ π β π) β π β V) |
41 | | ovexd 7393 |
. . 3
β’ ((π β π β§ π β π) β (π΅ βm π΄) β V) |
42 | | ovexd 7393 |
. . 3
β’ ((π β π β§ π β π) β (π΄ βm π΅) β V) |
43 | | simprll 778 |
. . 3
β’ (((π β π β§ π β π) β§ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))) β π β (π΅ βm π΄)) |
44 | | simprlr 779 |
. . 3
β’ (((π β π β§ π β π) β§ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))) β π β (π΄ βm π΅)) |
45 | 41, 42, 43, 44 | opabex2 7990 |
. 2
β’ ((π β π β§ π β π) β {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))} β V) |
46 | 2, 36, 38, 40, 45 | ovmpod 7508 |
1
β’ ((π β π β§ π β π) β (πMGalConnπ) = {β¨π, πβ© β£ ((π β (π΅ βm π΄) β§ π β (π΄ βm π΅)) β§ βπ₯ β π΄ βπ¦ β π΅ ((πβπ₯) β² π¦ β π₯ β€ (πβπ¦)))}) |