Metamath Proof Explorer

Theorem assa2ass

Description: Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019) (Proof shortened by Zhi Wang, 11-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 assa2ass.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 assa2ass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 assa2ass.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 assa2ass.m ⊢ ∗ = ( .r ‘ 𝐹 )
5 assa2ass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 assa2ass.t ⊢ × = ( .r ‘ 𝑊 )
7 simp1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ AssAlg )
8 simpr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
9 8 3ad2ant2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐶 ∈ 𝐵 )
10 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
11 simpl ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
12 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
13 1 2 5 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
14 10 11 12 13 syl3an ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
15 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
16 15 3ad2ant3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑌 ∈ 𝑉 )
17 1 2 3 5 6 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐶 ∈ 𝐵 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × ( 𝐶 · 𝑌 ) ) = ( 𝐶 · ( ( 𝐴 · 𝑋 ) × 𝑌 ) ) )
18 7 9 14 16 17 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × ( 𝐶 · 𝑌 ) ) = ( 𝐶 · ( ( 𝐴 · 𝑋 ) × 𝑌 ) ) )
19 1 2 3 5 6 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐶 ∈ 𝐵 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) = ( 𝐶 · ( ( 𝐴 · 𝑋 ) × 𝑌 ) ) )
20 19 eqcomd ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐶 ∈ 𝐵 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐶 · ( ( 𝐴 · 𝑋 ) × 𝑌 ) ) = ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) )
21 7 9 14 16 20 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐶 · ( ( 𝐴 · 𝑋 ) × 𝑌 ) ) = ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) )
22 10 3ad2ant1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
23 11 3ad2ant2 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐵 )
24 12 3ad2ant3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑋 ∈ 𝑉 )
25 1 2 5 3 4 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) = ( 𝐶 · ( 𝐴 · 𝑋 ) ) )
26 25 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐶 · ( 𝐴 · 𝑋 ) ) = ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) )
27 26 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) = ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) )
28 22 9 23 24 27 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) = ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) )
29 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
30 29 adantr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐹 ∈ Ring )
31 8 adantl ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
32 11 adantl ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 )
33 3 4 30 31 32 ringcld ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 )
34 33 3adant3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 )
35 1 2 3 5 6 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
36 7 34 24 16 35 syl13anc ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
37 28 36 eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
38 18 21 37 3eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × ( 𝐶 · 𝑌 ) ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )