Theorem lcdvsval

Description: Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvsval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvsval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcdvsval.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcdvsval.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcdvsval.t	⊢ · = ( .r ‘ 𝑆 )
	lcdvsval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsval.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
	lcdvsval.m	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	lcdvsval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvsval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
	lcdvsval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcdvsval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	lcdvsval	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvsval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvsval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvsval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		lcdvsval.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
5		lcdvsval.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
6		lcdvsval.t	⊢ · = ( .r ‘ 𝑆 )
7		lcdvsval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		lcdvsval.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
9		lcdvsval.m	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
10		lcdvsval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11		lcdvsval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
12		lcdvsval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
13		lcdvsval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
14		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
15		eqid	⊢ ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) = ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) )
16	1 2 14 15 7 9 10	lcdvs	⊢ ( 𝜑 → ∙ = ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) )
17	16	oveqd	⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝑋 ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝑋 ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) ‘ 𝐴 ) )
19		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
20	1 2 10	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
21	1 7 8 2 19 10 12	lcdvbaselfl	⊢ ( 𝜑 → 𝐺 ∈ ( LFnl ‘ 𝑈 ) )
22	19 3 4 5 6 14 15 20 11 21 13	ldualvsval	⊢ ( 𝜑 → ( ( 𝑋 ( ·𝑠 ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) · 𝑋 ) )
23	18 22	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) · 𝑋 ) )