Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) ∙ 𝐺 ) = ( 𝑋 ∙ ( 𝑌 ∙ 𝐺 ) ) )