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 ) ) )