Theorem lcdvadd

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

	Ref	Expression
Hypotheses	lcdvadd.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvadd.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcdvadd.a	⊢ + = ( +g ‘ 𝐷 )
	lcdvadd.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvadd.p	⊢ ✚ = ( +g ‘ 𝐶 )
	lcdvadd.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdvadd	⊢ ( 𝜑 → ✚ = + )

Proof

Step	Hyp	Ref	Expression
1		lcdvadd.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvadd.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
4		lcdvadd.a	⊢ + = ( +g ‘ 𝐷 )
5		lcdvadd.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		lcdvadd.p	⊢ ✚ = ( +g ‘ 𝐶 )
7		lcdvadd.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
10		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
11	1 8 5 2 9 10 3 7	lcdval	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
12	11	fveq2d	⊢ ( 𝜑 → ( +g ‘ 𝐶 ) = ( +g ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
13		fvex	⊢ ( LFnl ‘ 𝑈 ) ∈ V
14	13	rabex	⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V
15		eqid	⊢ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) = ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
16	15 4	ressplusg	⊢ ( { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ∈ V → + = ( +g ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) ) )
17	14 16	ax-mp	⊢ + = ( +g ‘ ( 𝐷 ↾s { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
18	12 6 17	3eqtr4g	⊢ ( 𝜑 → ✚ = + )