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

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 
|- V = ( Base ` W )
assa2ass.f 
|- F = ( Scalar ` W )
assa2ass.b 
|- B = ( Base ` F )
assa2ass.m 
|- .* = ( .r ` F )
assa2ass.s 
|- .x. = ( .s ` W )
assa2ass.t 
|- .X. = ( .r ` W )
Assertion assa2ass 
|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( C .* A ) .x. ( X .X. Y ) ) )

Proof

Step Hyp Ref Expression
1 assa2ass.v 
 |-  V = ( Base ` W )
2 assa2ass.f 
 |-  F = ( Scalar ` W )
3 assa2ass.b 
 |-  B = ( Base ` F )
4 assa2ass.m 
 |-  .* = ( .r ` F )
5 assa2ass.s 
 |-  .x. = ( .s ` W )
6 assa2ass.t 
 |-  .X. = ( .r ` W )
7 simp1 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> W e. AssAlg )
8 simpr 
 |-  ( ( A e. B /\ C e. B ) -> C e. B )
9 8 3ad2ant2 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> C e. B )
10 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
11 simpl 
 |-  ( ( A e. B /\ C e. B ) -> A e. B )
12 simpl 
 |-  ( ( X e. V /\ Y e. V ) -> X e. V )
13 1 2 5 3 lmodvscl 
 |-  ( ( W e. LMod /\ A e. B /\ X e. V ) -> ( A .x. X ) e. V )
14 10 11 12 13 syl3an 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( A .x. X ) e. V )
15 simpr 
 |-  ( ( X e. V /\ Y e. V ) -> Y e. V )
16 15 3ad2ant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
17 1 2 3 5 6 assaassr 
 |-  ( ( W e. AssAlg /\ ( C e. B /\ ( A .x. X ) e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( C .x. ( ( A .x. X ) .X. Y ) ) )
18 7 9 14 16 17 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( C .x. ( ( A .x. X ) .X. Y ) ) )
19 1 2 3 5 6 assaass 
 |-  ( ( W e. AssAlg /\ ( C e. B /\ ( A .x. X ) e. V /\ Y e. V ) ) -> ( ( C .x. ( A .x. X ) ) .X. Y ) = ( C .x. ( ( A .x. X ) .X. Y ) ) )
20 19 eqcomd 
 |-  ( ( W e. AssAlg /\ ( C e. B /\ ( A .x. X ) e. V /\ Y e. V ) ) -> ( C .x. ( ( A .x. X ) .X. Y ) ) = ( ( C .x. ( A .x. X ) ) .X. Y ) )
21 7 9 14 16 20 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( C .x. ( ( A .x. X ) .X. Y ) ) = ( ( C .x. ( A .x. X ) ) .X. Y ) )
22 10 3ad2ant1 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> W e. LMod )
23 11 3ad2ant2 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> A e. B )
24 12 3ad2ant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> X e. V )
25 1 2 5 3 4 lmodvsass 
 |-  ( ( W e. LMod /\ ( C e. B /\ A e. B /\ X e. V ) ) -> ( ( C .* A ) .x. X ) = ( C .x. ( A .x. X ) ) )
26 25 eqcomd 
 |-  ( ( W e. LMod /\ ( C e. B /\ A e. B /\ X e. V ) ) -> ( C .x. ( A .x. X ) ) = ( ( C .* A ) .x. X ) )
27 26 oveq1d 
 |-  ( ( W e. LMod /\ ( C e. B /\ A e. B /\ X e. V ) ) -> ( ( C .x. ( A .x. X ) ) .X. Y ) = ( ( ( C .* A ) .x. X ) .X. Y ) )
28 22 9 23 24 27 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( C .x. ( A .x. X ) ) .X. Y ) = ( ( ( C .* A ) .x. X ) .X. Y ) )
29 2 assasca 
 |-  ( W e. AssAlg -> F e. Ring )
30 29 adantr 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> F e. Ring )
31 8 adantl 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> C e. B )
32 11 adantl 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> A e. B )
33 3 4 30 31 32 ringcld 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> ( C .* A ) e. B )
34 33 3adant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( C .* A ) e. B )
35 1 2 3 5 6 assaass 
 |-  ( ( W e. AssAlg /\ ( ( C .* A ) e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( C .* A ) .x. X ) .X. Y ) = ( ( C .* A ) .x. ( X .X. Y ) ) )
36 7 34 24 16 35 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( C .* A ) .x. X ) .X. Y ) = ( ( C .* A ) .x. ( X .X. Y ) ) )
37 28 36 eqtrd 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( C .x. ( A .x. X ) ) .X. Y ) = ( ( C .* A ) .x. ( X .X. Y ) ) )
38 18 21 37 3eqtrd 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( C .* A ) .x. ( X .X. Y ) ) )