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

Metamath Proof Explorer

Theorem assa2ass2

Description: Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed 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 assa2ass2 
|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( A .* C ) .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 simpl 
 |-  ( ( A e. B /\ C e. B ) -> A e. B )
9 8 3ad2ant2 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> A e. B )
10 simpl 
 |-  ( ( X e. V /\ Y e. V ) -> X e. V )
11 10 3ad2ant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> X e. V )
12 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
13 12 3ad2ant1 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> W e. LMod )
14 simpr 
 |-  ( ( A e. B /\ C e. B ) -> C e. B )
15 14 3ad2ant2 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> C e. B )
16 simpr 
 |-  ( ( X e. V /\ Y e. V ) -> Y e. V )
17 16 3ad2ant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
18 1 2 5 3 13 15 17 lmodvscld 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( C .x. Y ) e. V )
19 1 2 3 5 6 assaass 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ ( C .x. Y ) e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( A .x. ( X .X. ( C .x. Y ) ) ) )
20 7 9 11 18 19 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( A .x. ( X .X. ( C .x. Y ) ) ) )
21 1 2 3 5 6 assaassr 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ ( C .x. Y ) e. V ) ) -> ( X .X. ( A .x. ( C .x. Y ) ) ) = ( A .x. ( X .X. ( C .x. Y ) ) ) )
22 21 eqcomd 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ ( C .x. Y ) e. V ) ) -> ( A .x. ( X .X. ( C .x. Y ) ) ) = ( X .X. ( A .x. ( C .x. Y ) ) ) )
23 7 9 11 18 22 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( A .x. ( X .X. ( C .x. Y ) ) ) = ( X .X. ( A .x. ( C .x. Y ) ) ) )
24 1 2 5 3 4 lmodvsass 
 |-  ( ( W e. LMod /\ ( A e. B /\ C e. B /\ Y e. V ) ) -> ( ( A .* C ) .x. Y ) = ( A .x. ( C .x. Y ) ) )
25 24 eqcomd 
 |-  ( ( W e. LMod /\ ( A e. B /\ C e. B /\ Y e. V ) ) -> ( A .x. ( C .x. Y ) ) = ( ( A .* C ) .x. Y ) )
26 25 oveq2d 
 |-  ( ( W e. LMod /\ ( A e. B /\ C e. B /\ Y e. V ) ) -> ( X .X. ( A .x. ( C .x. Y ) ) ) = ( X .X. ( ( A .* C ) .x. Y ) ) )
27 13 9 15 17 26 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( X .X. ( A .x. ( C .x. Y ) ) ) = ( X .X. ( ( A .* C ) .x. Y ) ) )
28 2 assasca 
 |-  ( W e. AssAlg -> F e. Ring )
29 28 adantr 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> F e. Ring )
30 8 adantl 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> A e. B )
31 14 adantl 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> C e. B )
32 3 4 29 30 31 ringcld 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> ( A .* C ) e. B )
33 32 3adant3 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( A .* C ) e. B )
34 1 2 3 5 6 assaassr 
 |-  ( ( W e. AssAlg /\ ( ( A .* C ) e. B /\ X e. V /\ Y e. V ) ) -> ( X .X. ( ( A .* C ) .x. Y ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) )
35 7 33 11 17 34 syl13anc 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( X .X. ( ( A .* C ) .x. Y ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) )
36 27 35 eqtrd 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( X .X. ( A .x. ( C .x. Y ) ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) )
37 20 23 36 3eqtrd 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. ( C .x. Y ) ) = ( ( A .* C ) .x. ( X .X. Y ) ) )