Theorem assa2ass

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

	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. CRing )
30		crngring	|- ( F e. CRing -> F e. Ring )
31	29 30	syl	|- ( W e. AssAlg -> F e. Ring )
32	31	adantr	|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> F e. Ring )
33	8	adantl	|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> C e. B )
34	11	adantl	|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> A e. B )
35	3 4	ringcl	|- ( ( F e. Ring /\ C e. B /\ A e. B ) -> ( C .* A ) e. B )
36	32 33 34 35	syl3anc	|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) ) -> ( C .* A ) e. B )
37	36	3adant3	|- ( ( W e. AssAlg /\ ( A e. B /\ C e. B ) /\ ( X e. V /\ Y e. V ) ) -> ( C .* A ) e. B )
38	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 ) ) )
39	7 37 24 16 38	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 ) ) )
40	28 39	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 ) ) )
41	18 21 40	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 ) ) )