Step | Hyp | Ref
| Expression |
1 | | dvhset.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
2 | | dvhset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | 2 | dvhfset 39481 |
. . . 4
β’ (πΎ β π β (DVecHβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) |
4 | 3 | fveq1d 6841 |
. . 3
β’ (πΎ β π β ((DVecHβπΎ)βπ) = ((π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))βπ)) |
5 | 1, 4 | eqtrid 2789 |
. 2
β’ (πΎ β π β π = ((π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))βπ)) |
6 | | fveq2 6839 |
. . . . . . . 8
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
7 | | dvhset.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
9 | | fveq2 6839 |
. . . . . . . 8
β’ (π€ = π β ((TEndoβπΎ)βπ€) = ((TEndoβπΎ)βπ)) |
10 | | dvhset.e |
. . . . . . . 8
β’ πΈ = ((TEndoβπΎ)βπ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((TEndoβπΎ)βπ€) = πΈ) |
12 | 8, 11 | xpeq12d 5662 |
. . . . . 6
β’ (π€ = π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) = (π Γ πΈ)) |
13 | 12 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β© = β¨(Baseβndx), (π Γ πΈ)β©) |
14 | 8 | mpteq1d 5198 |
. . . . . . . 8
β’ (π€ = π β (β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ))) = (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))) |
15 | 14 | opeq2d 4835 |
. . . . . . 7
β’ (π€ = π β β¨((1st βπ) β (1st
βπ)), (β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β© = β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) |
16 | 12, 12, 15 | mpoeq123dv 7426 |
. . . . . 6
β’ (π€ = π β (π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©) = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)) |
17 | 16 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β© =
β¨(+gβndx), (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©) |
18 | | fveq2 6839 |
. . . . . . 7
β’ (π€ = π β ((EDRingβπΎ)βπ€) = ((EDRingβπΎ)βπ)) |
19 | | dvhset.d |
. . . . . . 7
β’ π· = ((EDRingβπΎ)βπ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . 6
β’ (π€ = π β ((EDRingβπΎ)βπ€) = π·) |
21 | 20 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β© = β¨(Scalarβndx), π·β©) |
22 | 13, 17, 21 | tpeq123d 4707 |
. . . 4
β’ (π€ = π β {β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} = {β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©}) |
23 | | eqidd 2738 |
. . . . . . 7
β’ (π€ = π β β¨(π β(1st βπ)), (π β (2nd βπ))β© = β¨(π β(1st
βπ)), (π β (2nd
βπ))β©) |
24 | 11, 12, 23 | mpoeq123dv 7426 |
. . . . . 6
β’ (π€ = π β (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)) |
25 | 24 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β© = β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©) |
26 | 25 | sneqd 4596 |
. . . 4
β’ (π€ = π β {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©} = {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) |
27 | 22, 26 | uneq12d 4122 |
. . 3
β’ (π€ = π β ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) =
({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
28 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) = (π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
29 | | tpex 7673 |
. . . 4
β’
{β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} β
V |
30 | | snex 5386 |
. . . 4
β’ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©} β
V |
31 | 29, 30 | unex 7672 |
. . 3
β’
({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}) β
V |
32 | 27, 28, 31 | fvmpt 6945 |
. 2
β’ (π β π» β ((π€ β π» β¦ ({β¨(Baseβndx),
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx),
(π β
(((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
((EDRingβπΎ)βπ€)β©} βͺ {β¨(
Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))βπ) = ({β¨(Baseβndx),
(π Γ πΈ)β©,
β¨(+gβndx), (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |
33 | 5, 32 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx),
(π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
(β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx),
π·β©} βͺ {β¨(
Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) |