Step | Hyp | Ref
| Expression |
1 | | hvmapval.k |
. 2
β’ (π β (πΎ β π΄ β§ π β π»)) |
2 | | hvmapval.m |
. . . 4
β’ π = ((HVMapβπΎ)βπ) |
3 | | hvmapval.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
4 | 3 | hvmapffval 40271 |
. . . . 5
β’ (πΎ β π΄ β (HVMapβπΎ) = (π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))))))) |
5 | 4 | fveq1d 6848 |
. . . 4
β’ (πΎ β π΄ β ((HVMapβπΎ)βπ) = ((π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))))))βπ)) |
6 | 2, 5 | eqtrid 2785 |
. . 3
β’ (πΎ β π΄ β π = ((π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))))))βπ)) |
7 | | fveq2 6846 |
. . . . . . . . 9
β’ (π€ = π β ((DVecHβπΎ)βπ€) = ((DVecHβπΎ)βπ)) |
8 | | hvmapval.u |
. . . . . . . . 9
β’ π = ((DVecHβπΎ)βπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β ((DVecHβπΎ)βπ€) = π) |
10 | 9 | fveq2d 6850 |
. . . . . . 7
β’ (π€ = π β (Baseβ((DVecHβπΎ)βπ€)) = (Baseβπ)) |
11 | | hvmapval.v |
. . . . . . 7
β’ π = (Baseβπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (Baseβ((DVecHβπΎ)βπ€)) = π) |
13 | 9 | fveq2d 6850 |
. . . . . . . 8
β’ (π€ = π β
(0gβ((DVecHβπΎ)βπ€)) = (0gβπ)) |
14 | | hvmapval.z |
. . . . . . . 8
β’ 0 =
(0gβπ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β
(0gβ((DVecHβπΎ)βπ€)) = 0 ) |
16 | 15 | sneqd 4602 |
. . . . . 6
β’ (π€ = π β
{(0gβ((DVecHβπΎ)βπ€))} = { 0 }) |
17 | 12, 16 | difeq12d 4087 |
. . . . 5
β’ (π€ = π β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) = (π β { 0 })) |
18 | 9 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π€ = π β (Scalarβ((DVecHβπΎ)βπ€)) = (Scalarβπ)) |
19 | | hvmapval.s |
. . . . . . . . . 10
β’ π = (Scalarβπ) |
20 | 18, 19 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π€ = π β (Scalarβ((DVecHβπΎ)βπ€)) = π) |
21 | 20 | fveq2d 6850 |
. . . . . . . 8
β’ (π€ = π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€))) = (Baseβπ)) |
22 | | hvmapval.r |
. . . . . . . 8
β’ π
= (Baseβπ) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€))) = π
) |
24 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π€ = π β ((ocHβπΎ)βπ€) = ((ocHβπΎ)βπ)) |
25 | | hvmapval.o |
. . . . . . . . . 10
β’ π = ((ocHβπΎ)βπ) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π€ = π β ((ocHβπΎ)βπ€) = π) |
27 | 26 | fveq1d 6848 |
. . . . . . . 8
β’ (π€ = π β (((ocHβπΎ)βπ€)β{π₯}) = (πβ{π₯})) |
28 | 9 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π€ = π β
(+gβ((DVecHβπΎ)βπ€)) = (+gβπ)) |
29 | | hvmapval.p |
. . . . . . . . . . 11
β’ + =
(+gβπ) |
30 | 28, 29 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π€ = π β
(+gβ((DVecHβπΎ)βπ€)) = + ) |
31 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π€ = π β π‘ = π‘) |
32 | 9 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π€ = π β (
Β·π β((DVecHβπΎ)βπ€)) = ( Β·π
βπ)) |
33 | | hvmapval.t |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ) |
34 | 32, 33 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π€ = π β (
Β·π β((DVecHβπΎ)βπ€)) = Β· ) |
35 | 34 | oveqd 7378 |
. . . . . . . . . 10
β’ (π€ = π β (π( Β·π
β((DVecHβπΎ)βπ€))π₯) = (π Β· π₯)) |
36 | 30, 31, 35 | oveq123d 7382 |
. . . . . . . . 9
β’ (π€ = π β (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)) = (π‘ + (π Β· π₯))) |
37 | 36 | eqeq2d 2744 |
. . . . . . . 8
β’ (π€ = π β (π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)) β π£ = (π‘ + (π Β· π₯)))) |
38 | 27, 37 | rexeqbidv 3319 |
. . . . . . 7
β’ (π€ = π β (βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)) β βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))) |
39 | 23, 38 | riotaeqbidv 7320 |
. . . . . 6
β’ (π€ = π β (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))) = (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))) |
40 | 12, 39 | mpteq12dv 5200 |
. . . . 5
β’ (π€ = π β (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)))) = (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯))))) |
41 | 17, 40 | mpteq12dv 5200 |
. . . 4
β’ (π€ = π β (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))))) = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))))) |
42 | | eqid 2733 |
. . . 4
β’ (π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)))))) = (π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯)))))) |
43 | 11 | fvexi 6860 |
. . . . . 6
β’ π β V |
44 | 43 | difexi 5289 |
. . . . 5
β’ (π β { 0 }) β
V |
45 | 44 | mptex 7177 |
. . . 4
β’ (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯))))) β V |
46 | 41, 42, 45 | fvmpt 6952 |
. . 3
β’ (π β π» β ((π€ β π» β¦ (π₯ β ((Baseβ((DVecHβπΎ)βπ€)) β
{(0gβ((DVecHβπΎ)βπ€))}) β¦ (π£ β (Baseβ((DVecHβπΎ)βπ€)) β¦ (β©π β
(Baseβ(Scalarβ((DVecHβπΎ)βπ€)))βπ‘ β (((ocHβπΎ)βπ€)β{π₯})π£ = (π‘(+gβ((DVecHβπΎ)βπ€))(π( Β·π
β((DVecHβπΎ)βπ€))π₯))))))βπ) = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))))) |
47 | 6, 46 | sylan9eq 2793 |
. 2
β’ ((πΎ β π΄ β§ π β π») β π = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))))) |
48 | 1, 47 | syl 17 |
1
β’ (π β π = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ‘ β (πβ{π₯})π£ = (π‘ + (π Β· π₯)))))) |