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) (Proof shortened by AV, 18-Oct-2024)

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