Theorem rmodislmodlem

Description: Lemma for rmodislmod . This is the part of the proof of rmodislmod which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021)

	Ref	Expression
Hypotheses	rmodislmod.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
	rmodislmod.a	⊢ + = ( +g ‘ 𝑅 )
	rmodislmod.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
	rmodislmod.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
	rmodislmod.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	rmodislmod.p	⊢ ⨣ = ( +g ‘ 𝐹 )
	rmodislmod.t	⊢ × = ( .r ‘ 𝐹 )
	rmodislmod.u	⊢ 1 = ( 1r ‘ 𝐹 )
	rmodislmod.r	⊢ ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) )
	rmodislmod.m	⊢ ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) )
	rmodislmod.l	⊢ 𝐿 = ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ )
Assertion	rmodislmodlem	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rmodislmod.v	⊢ 𝑉 = ( Base ‘ 𝑅 )
2		rmodislmod.a	⊢ + = ( +g ‘ 𝑅 )
3		rmodislmod.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
4		rmodislmod.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
5		rmodislmod.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		rmodislmod.p	⊢ ⨣ = ( +g ‘ 𝐹 )
7		rmodislmod.t	⊢ × = ( .r ‘ 𝐹 )
8		rmodislmod.u	⊢ 1 = ( 1r ‘ 𝐹 )
9		rmodislmod.r	⊢ ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) )
10		rmodislmod.m	⊢ ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) )
11		rmodislmod.l	⊢ 𝐿 = ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ )
12		simprl	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) )
13	12	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) )
14	13	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) )
15		ralrot3	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) )
16	1	grpbn0	⊢ ( 𝑅 ∈ Grp → 𝑉 ≠ ∅ )
17	16	3ad2ant1	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝑉 ≠ ∅ )
18	9 17	ax-mp	⊢ 𝑉 ≠ ∅
19		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ) )
20	18 19	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) )
21		oveq1	⊢ ( 𝑞 = 𝑏 → ( 𝑞 × 𝑟 ) = ( 𝑏 × 𝑟 ) )
22	21	oveq2d	⊢ ( 𝑞 = 𝑏 → ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( 𝑤 · ( 𝑏 × 𝑟 ) ) )
23		oveq2	⊢ ( 𝑞 = 𝑏 → ( 𝑤 · 𝑞 ) = ( 𝑤 · 𝑏 ) )
24	23	oveq1d	⊢ ( 𝑞 = 𝑏 → ( ( 𝑤 · 𝑞 ) · 𝑟 ) = ( ( 𝑤 · 𝑏 ) · 𝑟 ) )
25	22 24	eqeq12d	⊢ ( 𝑞 = 𝑏 → ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ↔ ( 𝑤 · ( 𝑏 × 𝑟 ) ) = ( ( 𝑤 · 𝑏 ) · 𝑟 ) ) )
26		oveq2	⊢ ( 𝑟 = 𝑎 → ( 𝑏 × 𝑟 ) = ( 𝑏 × 𝑎 ) )
27	26	oveq2d	⊢ ( 𝑟 = 𝑎 → ( 𝑤 · ( 𝑏 × 𝑟 ) ) = ( 𝑤 · ( 𝑏 × 𝑎 ) ) )
28		oveq2	⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · 𝑏 ) · 𝑟 ) = ( ( 𝑤 · 𝑏 ) · 𝑎 ) )
29	27 28	eqeq12d	⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · ( 𝑏 × 𝑟 ) ) = ( ( 𝑤 · 𝑏 ) · 𝑟 ) ↔ ( 𝑤 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑤 · 𝑏 ) · 𝑎 ) ) )
30		oveq1	⊢ ( 𝑤 = 𝑐 → ( 𝑤 · ( 𝑏 × 𝑎 ) ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) )
31		oveq1	⊢ ( 𝑤 = 𝑐 → ( 𝑤 · 𝑏 ) = ( 𝑐 · 𝑏 ) )
32	31	oveq1d	⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · 𝑏 ) · 𝑎 ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
33	30 32	eqeq12d	⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑤 · 𝑏 ) · 𝑎 ) ↔ ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) ) )
34	25 29 33	rspc3v	⊢ ( ( 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) ) )
35	34	3com12	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) ) )
36	20 35	syl5com	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) ) )
37	15 36	sylbi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) ) )
38		eqcom	⊢ ( ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) ↔ ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
39	37 38	imbitrrdi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) ) )
40	14 39	syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) ) )
41	40	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) ) )
42	9 41	ax-mp	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) )
43	42	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) )
44	5 7	crngcom	⊢ ( ( 𝐹 ∈ CRing ∧ 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ) → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) )
45	44	3expb	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ) ) → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) )
46	45	expcom	⊢ ( ( 𝑏 ∈ 𝐾 ∧ 𝑎 ∈ 𝐾 ) → ( 𝐹 ∈ CRing → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) ) )
47	46	ancoms	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝐹 ∈ CRing → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) ) )
48	47	3adant3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝐹 ∈ CRing → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) ) )
49	48	impcom	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑏 × 𝑎 ) = ( 𝑎 × 𝑏 ) )
50	49	oveq2d	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑐 · ( 𝑏 × 𝑎 ) ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
51	43 50	eqtrd	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
52	10	a1i	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
53		oveq12	⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = 𝑏 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
54	53	ancoms	⊢ ( ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
55	54	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
56		simp2	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝐾 )
57		simp3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
58		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ V )
59	52 55 56 57 58	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 ∗ 𝑐 ) = ( 𝑐 · 𝑏 ) )
60	59	oveq2d	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) = ( 𝑎 ∗ ( 𝑐 · 𝑏 ) ) )
61		oveq12	⊢ ( ( 𝑣 = ( 𝑐 · 𝑏 ) ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
62	61	ancoms	⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑐 · 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
63	62	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑐 · 𝑏 ) ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
64		simp1	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
65		simpl1	⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · 𝑟 ) ∈ 𝑉 )
66	65	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
67	66	2ralimi	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
68		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
69	5	grpbn0	⊢ ( 𝐹 ∈ Grp → 𝐾 ≠ ∅ )
70	68 69	syl	⊢ ( 𝐹 ∈ Ring → 𝐾 ≠ ∅ )
71	70	3ad2ant2	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝐾 ≠ ∅ )
72	9 71	ax-mp	⊢ 𝐾 ≠ ∅
73		rspn0	⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
74	72 73	ax-mp	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
75		ralcom	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
76		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
77	18 76	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
78		oveq2	⊢ ( 𝑟 = 𝑏 → ( 𝑤 · 𝑟 ) = ( 𝑤 · 𝑏 ) )
79	78	eleq1d	⊢ ( 𝑟 = 𝑏 → ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ( 𝑤 · 𝑏 ) ∈ 𝑉 ) )
80	31	eleq1d	⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · 𝑏 ) ∈ 𝑉 ↔ ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
81	79 80	rspc2v	⊢ ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
82	77 81	syl5com	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
83	75 82	sylbi	⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
84	67 74 83	3syl	⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
85	84	3ad2ant3	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 ) )
86	9 85	ax-mp	⊢ ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 )
87	86	3adant1	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ 𝑉 )
88		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) ∈ V )
89	52 63 64 87 88	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑐 · 𝑏 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
90	60 89	eqtrd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
91	90	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) = ( ( 𝑐 · 𝑏 ) · 𝑎 ) )
92		oveq12	⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = ( 𝑎 × 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
93	92	ancoms	⊢ ( ( 𝑠 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
94	93	adantl	⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = ( 𝑎 × 𝑏 ) ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
95	5 7	ringcl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 × 𝑏 ) ∈ 𝐾 )
96	95	3expib	⊢ ( 𝐹 ∈ Ring → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 × 𝑏 ) ∈ 𝐾 ) )
97	96	3ad2ant2	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 × 𝑏 ) ∈ 𝐾 ) )
98	9 97	ax-mp	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 × 𝑏 ) ∈ 𝐾 )
99	98	3adant3	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 × 𝑏 ) ∈ 𝐾 )
100		ovexd	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 × 𝑏 ) ) ∈ V )
101	52 94 99 57 100	ovmpod	⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
102	101	adantl	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑐 · ( 𝑎 × 𝑏 ) ) )
103	51 91 102	3eqtr4rd	⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) )