Metamath Proof Explorer

Theorem hvmaplkr

Description: Kernel of the vector to functional map. TODO: make this become lcfrlem11 . (Contributed by NM, 29-Mar-2015)

Ref Expression
Hypotheses hvmaplkr.h ⊢ H = LHyp ⁡ K
hvmaplkr.o ⊢ O = ocH ⁡ K ⁡ W
hvmaplkr.u ⊢ U = DVecH ⁡ K ⁡ W
hvmaplkr.v ⊢ V = Base U
hvmaplkr.z ⊢ 0 ˙ = 0 U
hvmaplkr.l ⊢ L = LKer ⁡ U
hvmaplkr.m ⊢ M = HVMap ⁡ K ⁡ W
hvmaplkr.k ⊢ φ → K ∈ HL ∧ W ∈ H
hvmaplkr.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion hvmaplkr ⊢ φ → L ⁡ M ⁡ X = O ⁡ X

Proof

Step Hyp Ref Expression
1 hvmaplkr.h ⊢ H = LHyp ⁡ K
2 hvmaplkr.o ⊢ O = ocH ⁡ K ⁡ W
3 hvmaplkr.u ⊢ U = DVecH ⁡ K ⁡ W
4 hvmaplkr.v ⊢ V = Base U
5 hvmaplkr.z ⊢ 0 ˙ = 0 U
6 hvmaplkr.l ⊢ L = LKer ⁡ U
7 hvmaplkr.m ⊢ M = HVMap ⁡ K ⁡ W
8 hvmaplkr.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 hvmaplkr.x ⊢ φ → X ∈ V ∖ 0 ˙
10 eqid ⊢ + U = + U
11 eqid ⊢ ⋅ U = ⋅ U
12 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
13 eqid ⊢ Base Scalar ⁡ U = Base Scalar ⁡ U
14 1 3 2 4 10 11 5 12 13 7 8 hvmapfval ⊢ φ → M = x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x
15 14 fveq1d ⊢ φ → M ⁡ X = x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x ⁡ X
16 15 fveq2d ⊢ φ → L ⁡ M ⁡ X = L ⁡ x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x ⁡ X
17 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
18 eqid ⊢ LDual ⁡ U = LDual ⁡ U
19 eqid ⊢ 0 LDual ⁡ U = 0 LDual ⁡ U
20 eqid ⊢ f ∈ LFnl ⁡ U | O ⁡ O ⁡ L ⁡ f = L ⁡ f = f ∈ LFnl ⁡ U | O ⁡ O ⁡ L ⁡ f = L ⁡ f
21 eqid ⊢ x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x = x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x
22 1 2 3 4 10 11 12 13 5 17 6 18 19 20 21 8 9 lcfrlem11 ⊢ φ → L ⁡ x ∈ V ∖ 0 ˙ ⟼ v ∈ V ⟼ ι j ∈ Base Scalar ⁡ U | ∃ t ∈ O ⁡ x v = t + U j ⋅ U x ⁡ X = O ⁡ X
23 16 22 eqtrd ⊢ φ → L ⁡ M ⁡ X = O ⁡ X