Metamath Proof Explorer


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 syl6ibr ( ∀ 𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) → ( ( 𝑎𝐾𝑏𝐾𝑐𝑉 ) → ( ( 𝑐 · 𝑏 ) · 𝑎 ) = ( 𝑐 · ( 𝑏 × 𝑎 ) ) ) )
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 ∧ ( 𝑎𝐾𝑏𝐾𝑐𝑉 ) ) → ( ( 𝑎 × 𝑏 ) 𝑐 ) = ( 𝑎 ( 𝑏 𝑐 ) ) )