Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | polfval.p |
. . 3
β’ π =
(β₯πβπΎ) |
3 | | fveq2 6843 |
. . . . . . 7
β’ (β = πΎ β (Atomsββ) = (AtomsβπΎ)) |
4 | | polfval.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . 6
β’ (β = πΎ β (Atomsββ) = π΄) |
6 | 5 | pweqd 4578 |
. . . . 5
β’ (β = πΎ β π« (Atomsββ) = π« π΄) |
7 | | fveq2 6843 |
. . . . . . . . . 10
β’ (β = πΎ β (pmapββ) = (pmapβπΎ)) |
8 | | polfval.m |
. . . . . . . . . 10
β’ π = (pmapβπΎ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . 9
β’ (β = πΎ β (pmapββ) = π) |
10 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (β = πΎ β (ocββ) = (ocβπΎ)) |
11 | | polfval.o |
. . . . . . . . . . 11
β’ β₯ =
(ocβπΎ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (β = πΎ β (ocββ) = β₯ ) |
13 | 12 | fveq1d 6845 |
. . . . . . . . 9
β’ (β = πΎ β ((ocββ)βπ) = ( β₯ βπ)) |
14 | 9, 13 | fveq12d 6850 |
. . . . . . . 8
β’ (β = πΎ β ((pmapββ)β((ocββ)βπ)) = (πβ( β₯ βπ))) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((β = πΎ β§ π β π) β ((pmapββ)β((ocββ)βπ)) = (πβ( β₯ βπ))) |
16 | 15 | iineq2dv 4980 |
. . . . . 6
β’ (β = πΎ β β©
π β π ((pmapββ)β((ocββ)βπ)) = β©
π β π (πβ( β₯ βπ))) |
17 | 5, 16 | ineq12d 4174 |
. . . . 5
β’ (β = πΎ β ((Atomsββ) β© β©
π β π ((pmapββ)β((ocββ)βπ))) = (π΄ β© β©
π β π (πβ( β₯ βπ)))) |
18 | 6, 17 | mpteq12dv 5197 |
. . . 4
β’ (β = πΎ β (π β π« (Atomsββ) β¦ ((Atomsββ) β© β© π β π ((pmapββ)β((ocββ)βπ)))) = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
19 | | df-polarityN 38369 |
. . . 4
β’
β₯π = (β β V β¦ (π β π« (Atomsββ) β¦ ((Atomsββ) β© β© π β π ((pmapββ)β((ocββ)βπ))))) |
20 | 4 | fvexi 6857 |
. . . . . 6
β’ π΄ β V |
21 | 20 | pwex 5336 |
. . . . 5
β’ π«
π΄ β V |
22 | 21 | mptex 7174 |
. . . 4
β’ (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ)))) β V |
23 | 18, 19, 22 | fvmpt 6949 |
. . 3
β’ (πΎ β V β
(β₯πβπΎ) = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
24 | 2, 23 | eqtrid 2789 |
. 2
β’ (πΎ β V β π = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |
25 | 1, 24 | syl 17 |
1
β’ (πΎ β π΅ β π = (π β π« π΄ β¦ (π΄ β© β©
π β π (πβ( β₯ βπ))))) |