Metamath Proof Explorer

Theorem lcdvs

Description: Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdvs.h ⊢ H = LHyp ⁡ K
lcdvs.u ⊢ U = DVecH ⁡ K ⁡ W
lcdvs.d ⊢ D = LDual ⁡ U
lcdvs.t ⊢ · ˙ = ⋅ D
lcdvs.c ⊢ C = LCDual ⁡ K ⁡ W
lcdvs.m ⊢ ∙ ˙ = ⋅ C
lcdvs.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion lcdvs ⊢ φ → ∙ ˙ = · ˙

Proof

Step Hyp Ref Expression
1 lcdvs.h ⊢ H = LHyp ⁡ K
2 lcdvs.u ⊢ U = DVecH ⁡ K ⁡ W
3 lcdvs.d ⊢ D = LDual ⁡ U
4 lcdvs.t ⊢ · ˙ = ⋅ D
5 lcdvs.c ⊢ C = LCDual ⁡ K ⁡ W
6 lcdvs.m ⊢ ∙ ˙ = ⋅ C
7 lcdvs.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
9 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
10 eqid ⊢ LKer ⁡ U = LKer ⁡ U
11 1 8 5 2 9 10 3 7 lcdval ⊢ φ → C = D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
12 11 fveq2d ⊢ φ → ⋅ C = ⋅ D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
13 fvex ⊢ LFnl ⁡ U ∈ V
14 13 rabex ⊢ f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∈ V
15 eqid ⊢ D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
16 15 4 ressvsca ⊢ f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∈ V → · ˙ = ⋅ D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
17 14 16 ax-mp ⊢ · ˙ = ⋅ D ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
18 12 6 17 3eqtr4g ⊢ φ → ∙ ˙ = · ˙