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

Metamath Proof Explorer

Theorem assaassrd

Description: Right-associative property of an associative algebra, deduction version. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses assaassd.1 ⊢ 𝑉 = ( Base ‘ 𝑊 )
assaassd.2 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
assaassd.3 ⊢ 𝐵 = ( Base ‘ 𝐹 )
assaassd.4 ⊢ · = ( ·𝑠 ‘ 𝑊 )
assaassd.5 ⊢ × = ( .r ‘ 𝑊 )
assaassd.6 ⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
assaassd.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
assaassd.8 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
assaassd.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion assaassrd ( 𝜑 → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 assaassd.1 ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 assaassd.2 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 assaassd.3 ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 assaassd.4 ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 assaassd.5 ⊢ × = ( .r ‘ 𝑊 )
6 assaassd.6 ⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
7 assaassd.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8 assaassd.8 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 assaassd.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 1 2 3 4 5 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )
11 6 7 8 9 10 syl13anc ⊢ ( 𝜑 → ( 𝑋 × ( 𝐴 · 𝑌 ) ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )