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	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvsval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvsval.v	$$⊢V={\mathrm{Base}}_U$$
	lcdvsval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcdvsval.r	$$⊢R={\mathrm{Base}}_S$$
	lcdvsval.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	lcdvsval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvsval.f	$$⊢F={\mathrm{Base}}_C$$
	lcdvsval.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	lcdvsval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvsval.x	$$⊢\phi \to X\in R$$
	lcdvsval.g	$$⊢\phi \to G\in F$$
	lcdvsval.a	$$⊢\phi \to A\in V$$
Assertion	lcdvsval	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		lcdvsval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvsval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvsval.v	$$⊢V={\mathrm{Base}}_U$$
4		lcdvsval.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
5		lcdvsval.r	$$⊢R={\mathrm{Base}}_S$$
6		lcdvsval.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
7		lcdvsval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		lcdvsval.f	$$⊢F={\mathrm{Base}}_C$$
9		lcdvsval.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
10		lcdvsval.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		lcdvsval.x	$$⊢\phi \to X\in R$$
12		lcdvsval.g	$$⊢\phi \to G\in F$$
13		lcdvsval.a	$$⊢\phi \to A\in V$$
14		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
15		eqid	$$⊢{\cdot }_{\mathrm{LDual}\left(U\right)}={\cdot }_{\mathrm{LDual}\left(U\right)}$$
16	1 2 14 15 7 9 10	lcdvs	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{\mathrm{LDual}\left(U\right)}$$
17	16	oveqd	$$⊢\phi \to X\underset{\dot{}}{\bullet }G=X{\cdot }_{\mathrm{LDual}\left(U\right)}G$$
18	17	fveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=\left(X{\cdot }_{\mathrm{LDual}\left(U\right)}G\right)\left(A\right)$$
19		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
20	1 2 10	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
21	1 7 8 2 19 10 12	lcdvbaselfl	$$⊢\phi \to G\in \mathrm{LFnl}\left(U\right)$$
22	19 3 4 5 6 14 15 20 11 21 13	ldualvsval	$$⊢\phi \to \left(X{\cdot }_{\mathrm{LDual}\left(U\right)}G\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{·}X$$
23	18 22	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\bullet }G\right)\left(A\right)=G\left(A\right)\underset{\dot{}}{·}X$$