Theorem clmvscom

Description: Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	clmvscl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	clmvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmvscl.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	clmvscl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmvscom	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑄 · ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑄 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clmvscl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		clmvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		clmvscl.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		clmvscl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		ssel	⊢ ( 𝐾 ⊆ ℂ → ( 𝑄 ∈ 𝐾 → 𝑄 ∈ ℂ ) )
6		ssel	⊢ ( 𝐾 ⊆ ℂ → ( 𝑅 ∈ 𝐾 → 𝑅 ∈ ℂ ) )
7	5 6	anim12d	⊢ ( 𝐾 ⊆ ℂ → ( ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) → ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) )
8	2 4	clmsscn	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
9	7 8	syl11	⊢ ( ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ) → ( 𝑊 ∈ ℂMod → ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) )
10	9	3adant3	⊢ ( ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ ℂMod → ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) )
11	10	impcom	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
12		mulcom	⊢ ( ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 𝑄 · 𝑅 ) = ( 𝑅 · 𝑄 ) )
13	11 12	syl	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑄 · 𝑅 ) = ( 𝑅 · 𝑄 ) )
14	13	oveq1d	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 · 𝑅 ) · 𝑋 ) = ( ( 𝑅 · 𝑄 ) · 𝑋 ) )
15	1 2 3 4	clmvsass	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑄 · 𝑅 ) · 𝑋 ) = ( 𝑄 · ( 𝑅 · 𝑋 ) ) )
16		3ancoma	⊢ ( ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ↔ ( 𝑅 ∈ 𝐾 ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) )
17	1 2 3 4	clmvsass	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · 𝑄 ) · 𝑋 ) = ( 𝑅 · ( 𝑄 · 𝑋 ) ) )
18	16 17	sylan2b	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · 𝑄 ) · 𝑋 ) = ( 𝑅 · ( 𝑄 · 𝑋 ) ) )
19	14 15 18	3eqtr3d	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑄 · ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑄 · 𝑋 ) ) )