Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (π β π β π β V) |
2 | | oveq12 7360 |
. . . . . . 7
β’ ((π = π β§ π = π) β (π LMHom π) = (π LMHom π)) |
3 | 2 | anidms 567 |
. . . . . 6
β’ (π = π β (π LMHom π) = (π LMHom π)) |
4 | | mendval.b |
. . . . . 6
β’ π΅ = (π LMHom π) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = π β (π LMHom π) = π΅) |
6 | 5 | csbeq1d 3857 |
. . . 4
β’ (π = π β β¦(π LMHom π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) = β¦π΅ / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
7 | | ovex 7384 |
. . . . . 6
β’ (π LMHom π) β V |
8 | 5, 7 | eqeltrrdi 2847 |
. . . . 5
β’ (π = π β π΅ β V) |
9 | | simpr 485 |
. . . . . . . 8
β’ ((π = π β§ π = π΅) β π = π΅) |
10 | 9 | opeq2d 4835 |
. . . . . . 7
β’ ((π = π β§ π = π΅) β β¨(Baseβndx), πβ© = β¨(Baseβndx),
π΅β©) |
11 | | fveq2 6839 |
. . . . . . . . . . . 12
β’ (π = π β (+gβπ) = (+gβπ)) |
12 | 11 | ofeqd 7611 |
. . . . . . . . . . 11
β’ (π = π β βf
(+gβπ) =
βf (+gβπ)) |
13 | 12 | oveqdr 7379 |
. . . . . . . . . 10
β’ ((π = π β§ π = π΅) β (π₯ βf
(+gβπ)π¦) = (π₯ βf
(+gβπ)π¦)) |
14 | 9, 9, 13 | mpoeq123dv 7426 |
. . . . . . . . 9
β’ ((π = π β§ π = π΅) β (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))) |
15 | | mendval.p |
. . . . . . . . 9
β’ + = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦)) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π = π β§ π = π΅) β (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦)) = + ) |
17 | 16 | opeq2d 4835 |
. . . . . . 7
β’ ((π = π β§ π = π΅) β β¨(+gβndx),
(π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β© = β¨(+gβndx),
+
β©) |
18 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π = π β§ π = π΅) β (π₯ β π¦) = (π₯ β π¦)) |
19 | 9, 9, 18 | mpoeq123dv 7426 |
. . . . . . . . 9
β’ ((π = π β§ π = π΅) β (π₯ β π, π¦ β π β¦ (π₯ β π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))) |
20 | | mendval.t |
. . . . . . . . 9
β’ Γ =
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) |
21 | 19, 20 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π = π β§ π = π΅) β (π₯ β π, π¦ β π β¦ (π₯ β π¦)) = Γ ) |
22 | 21 | opeq2d 4835 |
. . . . . . 7
β’ ((π = π β§ π = π΅) β β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β© = β¨(.rβndx),
Γ
β©) |
23 | 10, 17, 22 | tpeq123d 4707 |
. . . . . 6
β’ ((π = π β§ π = π΅) β {β¨(Baseβndx), πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} = {β¨(Baseβndx), π΅β©,
β¨(+gβndx), + β©,
β¨(.rβndx), Γ
β©}) |
24 | | fveq2 6839 |
. . . . . . . . . 10
β’ (π = π β (Scalarβπ) = (Scalarβπ)) |
25 | 24 | adantr 481 |
. . . . . . . . 9
β’ ((π = π β§ π = π΅) β (Scalarβπ) = (Scalarβπ)) |
26 | | mendval.s |
. . . . . . . . 9
β’ π = (Scalarβπ) |
27 | 25, 26 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π = π β§ π = π΅) β (Scalarβπ) = π) |
28 | 27 | opeq2d 4835 |
. . . . . . 7
β’ ((π = π β§ π = π΅) β β¨(Scalarβndx),
(Scalarβπ)β© =
β¨(Scalarβndx), πβ©) |
29 | 27 | fveq2d 6843 |
. . . . . . . . . 10
β’ ((π = π β§ π = π΅) β (Baseβ(Scalarβπ)) = (Baseβπ)) |
30 | | fveq2 6839 |
. . . . . . . . . . . . 13
β’ (π = π β (
Β·π βπ) = ( Β·π
βπ)) |
31 | 30 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π΅) β (
Β·π βπ) = ( Β·π
βπ)) |
32 | 31 | ofeqd 7611 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π΅) β βf (
Β·π βπ) = βf (
Β·π βπ)) |
33 | | fveq2 6839 |
. . . . . . . . . . . . 13
β’ (π = π β (Baseβπ) = (Baseβπ)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = π΅) β (Baseβπ) = (Baseβπ)) |
35 | 34 | xpeq1d 5660 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π΅) β ((Baseβπ) Γ {π₯}) = ((Baseβπ) Γ {π₯})) |
36 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π΅) β π¦ = π¦) |
37 | 32, 35, 36 | oveq123d 7372 |
. . . . . . . . . 10
β’ ((π = π β§ π = π΅) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
38 | 29, 9, 37 | mpoeq123dv 7426 |
. . . . . . . . 9
β’ ((π = π β§ π = π΅) β (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) = (π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))) |
39 | | mendval.v |
. . . . . . . . 9
β’ Β· =
(π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
40 | 38, 39 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π = π β§ π = π΅) β (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) = Β· ) |
41 | 40 | opeq2d 4835 |
. . . . . . 7
β’ ((π = π β§ π = π΅) β β¨(
Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β© = β¨(
Β·π βndx), Β·
β©) |
42 | 28, 41 | preq12d 4700 |
. . . . . 6
β’ ((π = π β§ π = π΅) β {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©} = {β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©}) |
43 | 23, 42 | uneq12d 4122 |
. . . . 5
β’ ((π = π β§ π = π΅) β ({β¨(Baseβndx), πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) = ({β¨(Baseβndx), π΅β©,
β¨(+gβndx), + β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©})) |
44 | 8, 43 | csbied 3891 |
. . . 4
β’ (π = π β β¦π΅ / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) = ({β¨(Baseβndx), π΅β©,
β¨(+gβndx), + β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©})) |
45 | 6, 44 | eqtrd 2777 |
. . 3
β’ (π = π β β¦(π LMHom π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) = ({β¨(Baseβndx), π΅β©,
β¨(+gβndx), + β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©})) |
46 | | df-mend 41412 |
. . 3
β’ MEndo =
(π β V β¦
β¦(π LMHom
π) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
47 | | tpex 7673 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
+ β©,
β¨(.rβndx), Γ β©} β
V |
48 | | prex 5387 |
. . . 4
β’
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β· β©} β
V |
49 | 47, 48 | unex 7672 |
. . 3
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
+ β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β· β©}) β
V |
50 | 45, 46, 49 | fvmpt 6945 |
. 2
β’ (π β V β
(MEndoβπ) =
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
+ β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©})) |
51 | 1, 50 | syl 17 |
1
β’ (π β π β (MEndoβπ) = ({β¨(Baseβndx), π΅β©,
β¨(+gβndx), + β©,
β¨(.rβndx), Γ β©} βͺ
{β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), Β·
β©})) |