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	⊢ 𝑉 = ( 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 → 𝐹 ∈ CRing )
30		crngring	⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
31	29 30	syl	⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
32	31	adantr	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐹 ∈ Ring )
33	8	adantl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
34	11	adantl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 )
35	3 4	ringcl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 )
36	32 33 34 35	syl3anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 )
37	36	3adant3	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 )
38	1 2 3 5 6	assaass	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ( 𝐶 ∗ 𝐴 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
39	7 37 24 16 38	syl13anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐶 ∗ 𝐴 ) · 𝑋 ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
40	28 39	eqtrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐶 · ( 𝐴 · 𝑋 ) ) × 𝑌 ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )
41	18 21 40	3eqtrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝑋 ) × ( 𝐶 · 𝑌 ) ) = ( ( 𝐶 ∗ 𝐴 ) · ( 𝑋 × 𝑌 ) ) )

Metamath Proof Explorer

Theorem assa2ass

Proof