Step | Hyp | Ref
| Expression |
1 | | elex 3492 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | polfval.p |
. . 3
β’ π =
(β₯πβπΎ) |
3 | | fveq2 6891 |
. . . . . . 7
β’ (β = πΎ β (Atomsββ) = (AtomsβπΎ)) |
4 | | polfval.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2790 |
. . . . . 6
β’ (β = πΎ β (Atomsββ) = π΄) |
6 | 5 | pweqd 4619 |
. . . . 5
β’ (β = πΎ β π« (Atomsββ) = π« π΄) |
7 | | fveq2 6891 |
. . . . . . . . . 10
β’ (β = πΎ β (pmapββ) = (pmapβπΎ)) |
8 | | polfval.m |
. . . . . . . . . 10
β’ π = (pmapβπΎ) |
9 | 7, 8 | eqtr4di 2790 |
. . . . . . . . 9
β’ (β = πΎ β (pmapββ) = π) |
10 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (β = πΎ β (ocββ) = (ocβπΎ)) |
11 | | polfval.o |
. . . . . . . . . . 11
β’ β₯ =
(ocβπΎ) |
12 | 10, 11 | eqtr4di 2790 |
. . . . . . . . . 10
β’ (β = πΎ β (ocββ) = β₯ ) |
13 | 12 | fveq1d 6893 |
. . . . . . . . 9
β’ (β = πΎ β ((ocββ)βπ) = ( β₯ βπ)) |
14 | 9, 13 | fveq12d 6898 |
. . . . . . . 8
β’ (β = πΎ β ((pmapββ)β((ocββ)βπ)) = (πβ( β₯ βπ))) |
15 | 14 | adantr 481 |
. . . . . . 7
β’ ((β = πΎ β§ π β π) β ((pmapββ)β((ocββ)βπ)) = (πβ( β₯ βπ))) |
16 | 15 | iineq2dv 5022 |
. . . . . 6
β’ (β = πΎ β β©
π β π ((pmapββ)β((ocββ)βπ)) = β©
π β π (πβ( β₯ βπ))) |
17 | 5, 16 | ineq12d 4213 |
. . . . 5
β’ (β = πΎ β ((Atomsββ) β© β©
π β π ((pmapββ)β((ocββ)βπ))) = (π΄ β© β©
π β π (πβ( β₯ βπ)))) |
18 | 6, 17 | mpteq12dv 5239 |
. . . 4
β’ (β = πΎ β (π β π« (Atomsββ) β¦ ((Atomsββ) β© β© π β π ((pmapββ)β((ocββ)βπ)))) = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
19 | | df-polarityN 38769 |
. . . 4
β’
β₯π = (β β V β¦ (π β π« (Atomsββ) β¦ ((Atomsββ) β© β© π β π ((pmapββ)β((ocββ)βπ))))) |
20 | 4 | fvexi 6905 |
. . . . . 6
β’ π΄ β V |
21 | 20 | pwex 5378 |
. . . . 5
β’ π«
π΄ β V |
22 | 21 | mptex 7224 |
. . . 4
β’ (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ)))) β V |
23 | 18, 19, 22 | fvmpt 6998 |
. . 3
β’ (πΎ β V β
(β₯πβπΎ) = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
24 | 2, 23 | eqtrid 2784 |
. 2
β’ (πΎ β V β π = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
25 | 1, 24 | syl 17 |
1
β’ (πΎ β π΅ β π = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |