Step | Hyp | Ref
| Expression |
1 | | scaffval.a |
. 2
β’ β = (
Β·sf βπ) |
2 | | fveq2 6839 |
. . . . . . . 8
β’ (π€ = π β (Scalarβπ€) = (Scalarβπ)) |
3 | | scaffval.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β (Scalarβπ€) = πΉ) |
5 | 4 | fveq2d 6843 |
. . . . . 6
β’ (π€ = π β (Baseβ(Scalarβπ€)) = (BaseβπΉ)) |
6 | | scaffval.k |
. . . . . 6
β’ πΎ = (BaseβπΉ) |
7 | 5, 6 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β (Baseβ(Scalarβπ€)) = πΎ) |
8 | | fveq2 6839 |
. . . . . 6
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
9 | | scaffval.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β (Baseβπ€) = π΅) |
11 | | fveq2 6839 |
. . . . . . 7
β’ (π€ = π β (
Β·π βπ€) = ( Β·π
βπ)) |
12 | | scaffval.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . 6
β’ (π€ = π β (
Β·π βπ€) = Β· ) |
14 | 13 | oveqd 7368 |
. . . . 5
β’ (π€ = π β (π₯( Β·π
βπ€)π¦) = (π₯ Β· π¦)) |
15 | 7, 10, 14 | mpoeq123dv 7426 |
. . . 4
β’ (π€ = π β (π₯ β (Baseβ(Scalarβπ€)), π¦ β (Baseβπ€) β¦ (π₯( Β·π
βπ€)π¦)) = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦))) |
16 | | df-scaf 20278 |
. . . 4
β’
Β·sf = (π€ β V β¦ (π₯ β (Baseβ(Scalarβπ€)), π¦ β (Baseβπ€) β¦ (π₯( Β·π
βπ€)π¦))) |
17 | 6 | fvexi 6853 |
. . . . 5
β’ πΎ β V |
18 | 9 | fvexi 6853 |
. . . . 5
β’ π΅ β V |
19 | 12 | fvexi 6853 |
. . . . . . 7
β’ Β· β
V |
20 | 19 | rnex 7841 |
. . . . . 6
β’ ran Β· β
V |
21 | | p0ex 5337 |
. . . . . 6
β’ {β
}
β V |
22 | 20, 21 | unex 7672 |
. . . . 5
β’ (ran
Β·
βͺ {β
}) β V |
23 | | df-ov 7354 |
. . . . . . 7
β’ (π₯ Β· π¦) = ( Β· ββ¨π₯, π¦β©) |
24 | | fvrn0 6869 |
. . . . . . 7
β’ ( Β·
ββ¨π₯, π¦β©) β (ran Β· βͺ
{β
}) |
25 | 23, 24 | eqeltri 2834 |
. . . . . 6
β’ (π₯ Β· π¦) β (ran Β· βͺ
{β
}) |
26 | 25 | rgen2w 3067 |
. . . . 5
β’
βπ₯ β
πΎ βπ¦ β π΅ (π₯ Β· π¦) β (ran Β· βͺ
{β
}) |
27 | 17, 18, 22, 26 | mpoexw 8003 |
. . . 4
β’ (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) β V |
28 | 15, 16, 27 | fvmpt 6945 |
. . 3
β’ (π β V β (
Β·sf βπ) = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦))) |
29 | | fvprc 6831 |
. . . 4
β’ (Β¬
π β V β (
Β·sf βπ) = β
) |
30 | | fvprc 6831 |
. . . . . . 7
β’ (Β¬
π β V β
(Baseβπ) =
β
) |
31 | 9, 30 | eqtrid 2789 |
. . . . . 6
β’ (Β¬
π β V β π΅ = β
) |
32 | 31 | olcd 872 |
. . . . 5
β’ (Β¬
π β V β (πΎ = β
β¨ π΅ = β
)) |
33 | | 0mpo0 7434 |
. . . . 5
β’ ((πΎ = β
β¨ π΅ = β
) β (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) = β
) |
34 | 32, 33 | syl 17 |
. . . 4
β’ (Β¬
π β V β (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) = β
) |
35 | 29, 34 | eqtr4d 2780 |
. . 3
β’ (Β¬
π β V β (
Β·sf βπ) = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦))) |
36 | 28, 35 | pm2.61i 182 |
. 2
β’ (
Β·sf βπ) = (π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) |
37 | 1, 36 | eqtri 2765 |
1
β’ β =
(π₯ β πΎ, π¦ β π΅ β¦ (π₯ Β· π¦)) |