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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvsass.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsass.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lcdvsass.l	⊢ 𝐿 = ( Base ‘ 𝑅 )
	lcdvsass.t	⊢ · = ( .r ‘ 𝑅 )
	lcdvsass.d	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvsass.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
	lcdvsass.s	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
	lcdvsass.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvsass.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
	lcdvsass.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐿 )
	lcdvsass.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lcdvsass	⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) ∙ 𝐺 ) = ( 𝑋 ∙ ( 𝑌 ∙ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvsass.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvsass.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvsass.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4		lcdvsass.l	⊢ 𝐿 = ( Base ‘ 𝑅 )
5		lcdvsass.t	⊢ · = ( .r ‘ 𝑅 )
6		lcdvsass.d	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		lcdvsass.f	⊢ 𝐹 = ( Base ‘ 𝐶 )
8		lcdvsass.s	⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9		lcdvsass.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcdvsass.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
11		lcdvsass.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐿 )
12		lcdvsass.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
13		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
14		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝐶 ) ) = ( .r ‘ ( Scalar ‘ 𝐶 ) )
15	1 2 3 4 5 6 13 14 9 10 11	lcdsmul	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ ( Scalar ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 · 𝑋 ) )
16	15	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( .r ‘ ( Scalar ‘ 𝐶 ) ) 𝑌 ) ∙ 𝐺 ) = ( ( 𝑌 · 𝑋 ) ∙ 𝐺 ) )
17	1 6 9	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
18		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
19	1 2 3 4 6 13 18 9	lcdsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝐿 )
20	10 19	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
21	11 19	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
22	7 13 8 18 14	lmodvsass	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝐺 ∈ 𝐹 ) ) → ( ( 𝑋 ( .r ‘ ( Scalar ‘ 𝐶 ) ) 𝑌 ) ∙ 𝐺 ) = ( 𝑋 ∙ ( 𝑌 ∙ 𝐺 ) ) )
23	17 20 21 12 22	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 ( .r ‘ ( Scalar ‘ 𝐶 ) ) 𝑌 ) ∙ 𝐺 ) = ( 𝑋 ∙ ( 𝑌 ∙ 𝐺 ) ) )
24	16 23	eqtr3d	⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) ∙ 𝐺 ) = ( 𝑋 ∙ ( 𝑌 ∙ 𝐺 ) ) )