Metamath Proof Explorer

Theorem lcdvadd

Description: Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015)

Ref Expression
Hypotheses lcdvadd.h ⊢ H = LHyp ⁡ K
lcdvadd.u ⊢ U = DVecH ⁡ K ⁡ W
lcdvadd.d ⊢ D = LDual ⁡ U
lcdvadd.a ⊢ + ˙ = + D
lcdvadd.c ⊢ C = LCDual ⁡ K ⁡ W
lcdvadd.p ⊢ ✚ ˙ = + C
lcdvadd.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion lcdvadd ⊢ φ → ✚ ˙ = + ˙

Proof

Step Hyp Ref Expression
1 lcdvadd.h ⊢ H = LHyp ⁡ K
2 lcdvadd.u ⊢ U = DVecH ⁡ K ⁡ W
3 lcdvadd.d ⊢ D = LDual ⁡ U
4 lcdvadd.a ⊢ + ˙ = + D
5 lcdvadd.c ⊢ C = LCDual ⁡ K ⁡ W
6 lcdvadd.p ⊢ ✚ ˙ = + C
7 lcdvadd.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 ressplusg ⊢ 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 ⊢ φ → ✚ ˙ = + ˙