Theorem assaass

Description: Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	isassa.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	isassa.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isassa.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	isassa.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	isassa.t	⊢ × = ( .r ‘ 𝑊 )
Assertion	assaass	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isassa.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		isassa.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		isassa.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		isassa.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		isassa.t	⊢ × = ( .r ‘ 𝑊 )
6	1 2 3 4 5	assalem	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ∧ ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) ) )
7	6	simpld	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )