Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6846 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | dvaset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2791 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
6 | 5 | fveq1d 6848 |
. . . . . . 7
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
7 | 6 | opeq2d 4841 |
. . . . . 6
β’ (π = πΎ β β¨(Baseβndx),
((LTrnβπ)βπ€)β© =
β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©) |
8 | | eqidd 2734 |
. . . . . . . 8
β’ (π = πΎ β (π β π) = (π β π)) |
9 | 6, 6, 8 | mpoeq123dv 7436 |
. . . . . . 7
β’ (π = πΎ β (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π)) = (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))) |
10 | 9 | opeq2d 4841 |
. . . . . 6
β’ (π = πΎ β β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β© = β¨(+gβndx),
(π β
((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©) |
11 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (EDRingβπ) = (EDRingβπΎ)) |
12 | 11 | fveq1d 6848 |
. . . . . . 7
β’ (π = πΎ β ((EDRingβπ)βπ€) = ((EDRingβπΎ)βπ€)) |
13 | 12 | opeq2d 4841 |
. . . . . 6
β’ (π = πΎ β β¨(Scalarβndx),
((EDRingβπ)βπ€)β© = β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©) |
14 | 7, 10, 13 | tpeq123d 4713 |
. . . . 5
β’ (π = πΎ β {β¨(Baseβndx),
((LTrnβπ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} = {β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©}) |
15 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = πΎ β (TEndoβπ) = (TEndoβπΎ)) |
16 | 15 | fveq1d 6848 |
. . . . . . . 8
β’ (π = πΎ β ((TEndoβπ)βπ€) = ((TEndoβπΎ)βπ€)) |
17 | | eqidd 2734 |
. . . . . . . 8
β’ (π = πΎ β (π βπ) = (π βπ)) |
18 | 16, 6, 17 | mpoeq123dv 7436 |
. . . . . . 7
β’ (π = πΎ β (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ)) = (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))) |
19 | 18 | opeq2d 4841 |
. . . . . 6
β’ (π = πΎ β β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β© = β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©) |
20 | 19 | sneqd 4602 |
. . . . 5
β’ (π = πΎ β {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©} = {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}) |
21 | 14, 20 | uneq12d 4128 |
. . . 4
β’ (π = πΎ β ({β¨(Baseβndx),
((LTrnβπ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©}) = ({β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©})) |
22 | 4, 21 | mpteq12dv 5200 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ ({β¨(Baseβndx),
((LTrnβπ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©})) = (π€ β π» β¦ ({β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}))) |
23 | | df-dveca 39516 |
. . 3
β’ DVecA =
(π β V β¦ (π€ β (LHypβπ) β¦
({β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©}))) |
24 | 22, 23, 3 | mptfvmpt 7182 |
. 2
β’ (πΎ β V β
(DVecAβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}))) |
25 | 1, 24 | syl 17 |
1
β’ (πΎ β π β (DVecAβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}))) |