Metamath Proof Explorer

Theorem rmodislmod

Description: The right module R induces a left module L by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod of a left module, see also islmod . (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 rmodislmod ( 𝐹 ∈ CRing → 𝐿 ∈ LMod )

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 baseid ⊢ Base = Slot ( Base ‘ ndx )
13 df-base ⊢ Base = Slot 1
14 1nn ⊢ 1 ∈ ℕ
15 13 14 ndxarg ⊢ ( Base ‘ ndx ) = 1
16 1re ⊢ 1 ∈ ℝ
17 1lt6 ⊢ 1 < 6
18 16 17 ltneii ⊢ 1 ≠ 6
19 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
20 18 19 neeqtrri ⊢ 1 ≠ ( ·𝑠 ‘ ndx )
21 15 20 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
22 12 21 setsnid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
23 1 22 eqtri ⊢ 𝑉 = ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
24 11 eqcomi ⊢ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) = 𝐿
25 24 fveq2i ⊢ ( Base ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) = ( Base ‘ 𝐿 )
26 23 25 eqtri ⊢ 𝑉 = ( Base ‘ 𝐿 )
27 26 a1i ⊢ ( 𝐹 ∈ CRing → 𝑉 = ( Base ‘ 𝐿 ) )
28 plusgid ⊢ +g = Slot ( +g ‘ ndx )
29 plusgndx ⊢ ( +g ‘ ndx ) = 2
30 2re ⊢ 2 ∈ ℝ
31 2lt6 ⊢ 2 < 6
32 30 31 ltneii ⊢ 2 ≠ 6
33 32 19 neeqtrri ⊢ 2 ≠ ( ·𝑠 ‘ ndx )
34 29 33 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
35 28 34 setsnid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
36 11 fveq2i ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
37 35 2 36 3eqtr4i ⊢ + = ( +g ‘ 𝐿 )
38 37 a1i ⊢ ( 𝐹 ∈ CRing → + = ( +g ‘ 𝐿 ) )
39 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
40 scandx ⊢ ( Scalar ‘ ndx ) = 5
41 5re ⊢ 5 ∈ ℝ
42 5lt6 ⊢ 5 < 6
43 41 42 ltneii ⊢ 5 ≠ 6
44 43 19 neeqtrri ⊢ 5 ≠ ( ·𝑠 ‘ ndx )
45 40 44 eqnetri ⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
46 39 45 setsnid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
47 11 fveq2i ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
48 46 4 47 3eqtr4i ⊢ 𝐹 = ( Scalar ‘ 𝐿 )
49 48 a1i ⊢ ( 𝐹 ∈ CRing → 𝐹 = ( Scalar ‘ 𝐿 ) )
50 9 simp1i ⊢ 𝑅 ∈ Grp
51 5 fvexi ⊢ 𝐾 ∈ V
52 1 fvexi ⊢ 𝑉 ∈ V
53 10 mpoexg ⊢ ( ( 𝐾 ∈ V ∧ 𝑉 ∈ V ) → ∗ ∈ V )
54 51 52 53 mp2an ⊢ ∗ ∈ V
55 vscaid ⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
56 55 setsid ⊢ ( ( 𝑅 ∈ Grp ∧ ∗ ∈ V ) → ∗ = ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) )
57 50 54 56 mp2an ⊢ ∗ = ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) )
58 24 fveq2i ⊢ ( ·𝑠 ‘ ( 𝑅 sSet ⟨ ( ·𝑠 ‘ ndx ) , ∗ ⟩ ) ) = ( ·𝑠 ‘ 𝐿 )
59 57 58 eqtri ⊢ ∗ = ( ·𝑠 ‘ 𝐿 )
60 59 a1i ⊢ ( 𝐹 ∈ CRing → ∗ = ( ·𝑠 ‘ 𝐿 ) )
61 5 a1i ⊢ ( 𝐹 ∈ CRing → 𝐾 = ( Base ‘ 𝐹 ) )
62 6 a1i ⊢ ( 𝐹 ∈ CRing → ⨣ = ( +g ‘ 𝐹 ) )
63 7 a1i ⊢ ( 𝐹 ∈ CRing → × = ( .r ‘ 𝐹 ) )
64 8 a1i ⊢ ( 𝐹 ∈ CRing → 1 = ( 1r ‘ 𝐹 ) )
65 crngring ⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
66 1 eqcomi ⊢ ( Base ‘ 𝑅 ) = 𝑉
67 66 26 eqtri ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐿 )
68 35 36 eqtr4i ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝐿 )
69 67 68 grpprop ⊢ ( 𝑅 ∈ Grp ↔ 𝐿 ∈ Grp )
70 50 69 mpbi ⊢ 𝐿 ∈ Grp
71 70 a1i ⊢ ( 𝐹 ∈ CRing → 𝐿 ∈ Grp )
72 10 a1i ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
73 oveq12 ⊢ ( ( 𝑣 = 𝑏 ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
74 73 ancoms ⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
75 74 adantl ⊢ ( ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
76 simp2 ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
77 simp3 ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
78 ovexd ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ V )
79 72 75 76 77 78 ovmpod ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) = ( 𝑏 · 𝑎 ) )
80 simpl1 ⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · 𝑟 ) ∈ 𝑉 )
81 80 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
82 81 2ralimi ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
83 ringgrp ⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
84 5 grpbn0 ⊢ ( 𝐹 ∈ Grp → 𝐾 ≠ ∅ )
85 83 84 syl ⊢ ( 𝐹 ∈ Ring → 𝐾 ≠ ∅ )
86 85 3ad2ant2 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝐾 ≠ ∅ )
87 9 86 ax-mp ⊢ 𝐾 ≠ ∅
88 rspn0 ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
89 87 88 ax-mp ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
90 ralcom ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
91 1 grpbn0 ⊢ ( 𝑅 ∈ Grp → 𝑉 ≠ ∅ )
92 91 3ad2ant1 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → 𝑉 ≠ ∅ )
93 9 92 ax-mp ⊢ 𝑉 ≠ ∅
94 rspn0 ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 ) )
95 93 94 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 )
96 oveq2 ⊢ ( 𝑟 = 𝑎 → ( 𝑤 · 𝑟 ) = ( 𝑤 · 𝑎 ) )
97 96 eleq1d ⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ↔ ( 𝑤 · 𝑎 ) ∈ 𝑉 ) )
98 oveq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 · 𝑎 ) = ( 𝑏 · 𝑎 ) )
99 98 eleq1d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 · 𝑎 ) ∈ 𝑉 ↔ ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
100 97 99 rspc2v ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
101 100 3adant1 ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
102 95 101 syl5com ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
103 90 102 sylbi ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 𝑟 ) ∈ 𝑉 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
104 82 89 103 3syl ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
105 104 3ad2ant3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 ) )
106 9 105 ax-mp ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ 𝑉 )
107 79 106 eqeltrd ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) ∈ 𝑉 )
108 10 a1i ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
109 oveq12 ⊢ ( ( 𝑣 = ( 𝑏 + 𝑐 ) ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
110 109 ancoms ⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑏 + 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
111 110 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = ( 𝑏 + 𝑐 ) ) ) → ( 𝑣 · 𝑠 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
112 simp1 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
113 1 2 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
114 50 113 mp3an1 ⊢ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
115 114 3adant1 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 + 𝑐 ) ∈ 𝑉 )
116 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) ∈ V )
117 108 111 112 115 116 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
118 simpl2 ⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
119 118 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
120 119 2ralimi ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
121 rspn0 ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ) )
122 87 121 ax-mp ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) )
123 oveq2 ⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 + 𝑥 ) · 𝑎 ) )
124 oveq2 ⊢ ( 𝑟 = 𝑎 → ( 𝑥 · 𝑟 ) = ( 𝑥 · 𝑎 ) )
125 96 124 oveq12d ⊢ ( 𝑟 = 𝑎 → ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) )
126 123 125 eqeq12d ⊢ ( 𝑟 = 𝑎 → ( ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ↔ ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) ) )
127 oveq2 ⊢ ( 𝑥 = 𝑐 → ( 𝑤 + 𝑥 ) = ( 𝑤 + 𝑐 ) )
128 127 oveq1d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 + 𝑐 ) · 𝑎 ) )
129 oveq1 ⊢ ( 𝑥 = 𝑐 → ( 𝑥 · 𝑎 ) = ( 𝑐 · 𝑎 ) )
130 129 oveq2d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
131 128 130 eqeq12d ⊢ ( 𝑥 = 𝑐 → ( ( ( 𝑤 + 𝑥 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑥 · 𝑎 ) ) ↔ ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
132 oveq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 + 𝑐 ) = ( 𝑏 + 𝑐 ) )
133 132 oveq1d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 + 𝑐 ) · 𝑎 ) )
134 98 oveq1d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
135 133 134 eqeq12d ⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 + 𝑐 ) · 𝑎 ) = ( ( 𝑤 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ↔ ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
136 126 131 135 rspc3v ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
137 136 3com23 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
138 122 137 syl5com ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
139 120 138 syl ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
140 139 3ad2ant3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) ) )
141 9 140 ax-mp ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 + 𝑐 ) · 𝑎 ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
142 117 141 eqtrd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
143 142 adantl ⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
144 74 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑏 · 𝑎 ) )
145 simp2 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
146 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 · 𝑎 ) ∈ V )
147 108 144 112 145 146 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑏 ) = ( 𝑏 · 𝑎 ) )
148 oveq12 ⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
149 148 ancoms ⊢ ( ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
150 149 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
151 simp3 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
152 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑎 ) ∈ V )
153 108 150 112 151 152 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑐 ) = ( 𝑐 · 𝑎 ) )
154 147 153 oveq12d ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
155 154 adantl ⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) = ( ( 𝑏 · 𝑎 ) + ( 𝑐 · 𝑎 ) ) )
156 143 155 eqtr4d ⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∗ ( 𝑏 + 𝑐 ) ) = ( ( 𝑎 ∗ 𝑏 ) + ( 𝑎 ∗ 𝑐 ) ) )
157 simpl3 ⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
158 157 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
159 158 2ralimi ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
160 ralrot3 ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
161 rspn0 ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) )
162 93 161 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) )
163 oveq1 ⊢ ( 𝑞 = 𝑎 → ( 𝑞 ⨣ 𝑟 ) = ( 𝑎 ⨣ 𝑟 ) )
164 163 oveq2d ⊢ ( 𝑞 = 𝑎 → ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) )
165 oveq2 ⊢ ( 𝑞 = 𝑎 → ( 𝑤 · 𝑞 ) = ( 𝑤 · 𝑎 ) )
166 165 oveq1d ⊢ ( 𝑞 = 𝑎 → ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) )
167 164 166 eqeq12d ⊢ ( 𝑞 = 𝑎 → ( ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ↔ ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) ) )
168 oveq2 ⊢ ( 𝑟 = 𝑏 → ( 𝑎 ⨣ 𝑟 ) = ( 𝑎 ⨣ 𝑏 ) )
169 168 oveq2d ⊢ ( 𝑟 = 𝑏 → ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) )
170 oveq2 ⊢ ( 𝑟 = 𝑏 → ( 𝑤 · 𝑟 ) = ( 𝑤 · 𝑏 ) )
171 170 oveq2d ⊢ ( 𝑟 = 𝑏 → ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) )
172 169 171 eqeq12d ⊢ ( 𝑟 = 𝑏 → ( ( 𝑤 · ( 𝑎 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑟 ) ) ↔ ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) ) )
173 oveq1 ⊢ ( 𝑤 = 𝑐 → ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
174 oveq1 ⊢ ( 𝑤 = 𝑐 → ( 𝑤 · 𝑎 ) = ( 𝑐 · 𝑎 ) )
175 oveq1 ⊢ ( 𝑤 = 𝑐 → ( 𝑤 · 𝑏 ) = ( 𝑐 · 𝑏 ) )
176 174 175 oveq12d ⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
177 173 176 eqeq12d ⊢ ( 𝑤 = 𝑐 → ( ( 𝑤 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑤 · 𝑎 ) + ( 𝑤 · 𝑏 ) ) ↔ ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
178 167 172 177 rspc3v ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
179 162 178 syl5com ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
180 160 179 sylbi ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
181 159 180 syl ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
182 181 3ad2ant3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) ) )
183 9 182 ax-mp ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
184 10 a1i ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
185 oveq12 ⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = ( 𝑎 ⨣ 𝑏 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
186 185 ancoms ⊢ ( ( 𝑠 = ( 𝑎 ⨣ 𝑏 ) ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
187 186 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = ( 𝑎 ⨣ 𝑏 ) ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
188 5 6 grpcl ⊢ ( ( 𝐹 ∈ Grp ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
189 188 3expib ⊢ ( 𝐹 ∈ Grp → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
190 83 189 syl ⊢ ( 𝐹 ∈ Ring → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
191 190 3ad2ant2 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 ) )
192 9 191 ax-mp ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
193 192 3adant3 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝐾 )
194 simp3 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
195 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) ∈ V )
196 184 187 193 194 195 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( 𝑐 · ( 𝑎 ⨣ 𝑏 ) ) )
197 149 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑎 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑎 ) )
198 simp1 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑎 ∈ 𝐾 )
199 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑎 ) ∈ V )
200 184 197 198 194 199 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 ∗ 𝑐 ) = ( 𝑐 · 𝑎 ) )
201 oveq12 ⊢ ( ( 𝑣 = 𝑐 ∧ 𝑠 = 𝑏 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
202 201 ancoms ⊢ ( ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
203 202 adantl ⊢ ( ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ∧ ( 𝑠 = 𝑏 ∧ 𝑣 = 𝑐 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑐 · 𝑏 ) )
204 simp2 ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → 𝑏 ∈ 𝐾 )
205 ovexd ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 · 𝑏 ) ∈ V )
206 184 203 204 194 205 ovmpod ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑏 ∗ 𝑐 ) = ( 𝑐 · 𝑏 ) )
207 200 206 oveq12d ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) = ( ( 𝑐 · 𝑎 ) + ( 𝑐 · 𝑏 ) ) )
208 183 196 207 3eqtr4d ⊢ ( ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) )
209 208 adantl ⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 ⨣ 𝑏 ) ∗ 𝑐 ) = ( ( 𝑎 ∗ 𝑐 ) + ( 𝑏 ∗ 𝑐 ) ) )
210 1 2 3 4 5 6 7 8 9 10 11 rmodislmodlem ⊢ ( ( 𝐹 ∈ CRing ∧ ( 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑎 × 𝑏 ) ∗ 𝑐 ) = ( 𝑎 ∗ ( 𝑏 ∗ 𝑐 ) ) )
211 10 a1i ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ∗ = ( 𝑠 ∈ 𝐾 , 𝑣 ∈ 𝑉 ↦ ( 𝑣 · 𝑠 ) ) )
212 oveq12 ⊢ ( ( 𝑣 = 𝑎 ∧ 𝑠 = 1 ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
213 212 ancoms ⊢ ( ( 𝑠 = 1 ∧ 𝑣 = 𝑎 ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
214 213 adantl ⊢ ( ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑠 = 1 ∧ 𝑣 = 𝑎 ) ) → ( 𝑣 · 𝑠 ) = ( 𝑎 · 1 ) )
215 5 8 ringidcl ⊢ ( 𝐹 ∈ Ring → 1 ∈ 𝐾 )
216 65 215 syl ⊢ ( 𝐹 ∈ CRing → 1 ∈ 𝐾 )
217 216 adantr ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → 1 ∈ 𝐾 )
218 simpr ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
219 ovexd ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) ∈ V )
220 211 214 217 218 219 ovmpod ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 1 ∗ 𝑎 ) = ( 𝑎 · 1 ) )
221 simprr ⊢ ( ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( 𝑤 · 1 ) = 𝑤 )
222 221 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
223 222 2ralimi ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
224 rspn0 ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
225 87 224 ax-mp ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
226 rspn0 ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
227 87 226 ax-mp ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
228 rspn0 ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 ) )
229 93 228 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 )
230 oveq1 ⊢ ( 𝑤 = 𝑎 → ( 𝑤 · 1 ) = ( 𝑎 · 1 ) )
231 id ⊢ ( 𝑤 = 𝑎 → 𝑤 = 𝑎 )
232 230 231 eqeq12d ⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 · 1 ) = 𝑤 ↔ ( 𝑎 · 1 ) = 𝑎 ) )
233 232 rspcv ⊢ ( 𝑎 ∈ 𝑉 → ( ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( 𝑎 · 1 ) = 𝑎 ) )
234 233 adantl ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( 𝑎 · 1 ) = 𝑎 ) )
235 229 234 syl5com ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
236 227 235 syl ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( 𝑤 · 1 ) = 𝑤 → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
237 223 225 236 3syl ⊢ ( ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
238 237 3ad2ant3 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( ( 𝑤 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑤 + 𝑥 ) · 𝑟 ) = ( ( 𝑤 · 𝑟 ) + ( 𝑥 · 𝑟 ) ) ∧ ( 𝑤 · ( 𝑞 ⨣ 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) + ( 𝑤 · 𝑟 ) ) ) ∧ ( ( 𝑤 · ( 𝑞 × 𝑟 ) ) = ( ( 𝑤 · 𝑞 ) · 𝑟 ) ∧ ( 𝑤 · 1 ) = 𝑤 ) ) ) → ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 ) )
239 9 238 ax-mp ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 · 1 ) = 𝑎 )
240 220 239 eqtrd ⊢ ( ( 𝐹 ∈ CRing ∧ 𝑎 ∈ 𝑉 ) → ( 1 ∗ 𝑎 ) = 𝑎 )
241 27 38 49 60 61 62 63 64 65 71 107 156 209 210 240 islmodd ⊢ ( 𝐹 ∈ CRing → 𝐿 ∈ LMod )