This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem assaassr

Description: Right-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 assaassr ( ( 𝑊 ∈ 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 simprd ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )