Theorem lcdvsass

Description: Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcdvsass.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvsass.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvsass.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	lcdvsass.l	$$⊢L={\mathrm{Base}}_R$$
	lcdvsass.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	lcdvsass.d	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvsass.f	$$⊢F={\mathrm{Base}}_C$$
	lcdvsass.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	lcdvsass.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvsass.x	$$⊢\phi \to X\in L$$
	lcdvsass.y	$$⊢\phi \to Y\in L$$
	lcdvsass.g	$$⊢\phi \to G\in F$$
Assertion	lcdvsass	$$⊢\phi \to \left(Y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\bullet }G=X\underset{\dot{}}{\bullet }\left(Y\underset{\dot{}}{\bullet }G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcdvsass.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvsass.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvsass.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		lcdvsass.l	$$⊢L={\mathrm{Base}}_R$$
5		lcdvsass.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		lcdvsass.d	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		lcdvsass.f	$$⊢F={\mathrm{Base}}_C$$
8		lcdvsass.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		lcdvsass.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcdvsass.x	$$⊢\phi \to X\in L$$
11		lcdvsass.y	$$⊢\phi \to Y\in L$$
12		lcdvsass.g	$$⊢\phi \to G\in F$$
13		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
14		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(C\right)}={\cdot }_{\mathrm{Scalar}\left(C\right)}$$
15	1 2 3 4 5 6 13 14 9 10 11	lcdsmul	$$⊢\phi \to X{\cdot }_{\mathrm{Scalar}\left(C\right)}Y=Y\underset{\dot{}}{·}X$$
16	15	oveq1d	$$⊢\phi \to \left(X{\cdot }_{\mathrm{Scalar}\left(C\right)}Y\right)\underset{\dot{}}{\bullet }G=\left(Y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\bullet }G$$
17	1 6 9	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
18		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
19	1 2 3 4 6 13 18 9	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=L$$
20	10 19	eleqtrrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
21	11 19	eleqtrrd	$$⊢\phi \to Y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
22	7 13 8 18 14	lmodvsass	$$⊢\left(C\in \mathrm{LMod}\wedge \left(X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\wedge Y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\wedge G\in F\right)\right)\to \left(X{\cdot }_{\mathrm{Scalar}\left(C\right)}Y\right)\underset{\dot{}}{\bullet }G=X\underset{\dot{}}{\bullet }\left(Y\underset{\dot{}}{\bullet }G\right)$$
23	17 20 21 12 22	syl13anc	$$⊢\phi \to \left(X{\cdot }_{\mathrm{Scalar}\left(C\right)}Y\right)\underset{\dot{}}{\bullet }G=X\underset{\dot{}}{\bullet }\left(Y\underset{\dot{}}{\bullet }G\right)$$
24	16 23	eqtr3d	$$⊢\phi \to \left(Y\underset{\dot{}}{·}X\right)\underset{\dot{}}{\bullet }G=X\underset{\dot{}}{\bullet }\left(Y\underset{\dot{}}{\bullet }G\right)$$