MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rmodislmodOLD Structured version   Visualization version   GIF version

Theorem rmodislmodOLD 20391
Description: Obsolete version of rmodislmod 20390 as of 18-Oct-2024. The right module 𝑅 induces a left module 𝐿 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 20324 of a left module, see also islmod 20326. (Contributed by AV, 3-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
rmodislmodOLD (𝐹 ∈ CRing → 𝐿 ∈ LMod)
Distinct variable groups:   × ,𝑞,𝑟,𝑤,𝑥   × ,𝑠,𝑣   · ,𝑞,𝑟,𝑤,𝑥   · ,𝑠,𝑣   𝐾,𝑞,𝑟,𝑥   𝐾,𝑠,𝑣   𝑉,𝑞,𝑟,𝑤,𝑥   𝑉,𝑠,𝑣   𝐹,𝑠,𝑣   1 ,𝑠,𝑣   1 ,𝑞,𝑟,𝑤,𝑥   + ,𝑞,𝑟,𝑤,𝑥   + ,𝑠,𝑣   ,𝑞,𝑟,𝑤,𝑥   ,𝑠,𝑣
Allowed substitution hints:   𝑅(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞)   𝐹(𝑥,𝑤,𝑟,𝑞)   (𝑥,𝑤,𝑣,𝑠,𝑟,𝑞)   𝐾(𝑤)   𝐿(𝑥,𝑤,𝑣,𝑠,𝑟,𝑞)

Proof of Theorem rmodislmodOLD
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rmodislmod.v . . . . 5 𝑉 = (Base‘𝑅)
2 baseid 17086 . . . . . 6 Base = Slot (Base‘ndx)
3 df-base 17084 . . . . . . . 8 Base = Slot 1
4 1nn 12164 . . . . . . . 8 1 ∈ ℕ
53, 4ndxarg 17068 . . . . . . 7 (Base‘ndx) = 1
6 1re 11155 . . . . . . . . 9 1 ∈ ℝ
7 1lt6 12338 . . . . . . . . 9 1 < 6
86, 7ltneii 11268 . . . . . . . 8 1 ≠ 6
9 vscandx 17200 . . . . . . . 8 ( ·𝑠 ‘ndx) = 6
108, 9neeqtrri 3017 . . . . . . 7 1 ≠ ( ·𝑠 ‘ndx)
115, 10eqnetri 3014 . . . . . 6 (Base‘ndx) ≠ ( ·𝑠 ‘ndx)
122, 11setsnid 17081 . . . . 5 (Base‘𝑅) = (Base‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
131, 12eqtri 2764 . . . 4 𝑉 = (Base‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
14 rmodislmod.l . . . . . 6 𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)
1514eqcomi 2745 . . . . 5 (𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩) = 𝐿
1615fveq2i 6845 . . . 4 (Base‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)) = (Base‘𝐿)
1713, 16eqtri 2764 . . 3 𝑉 = (Base‘𝐿)
1817a1i 11 . 2 (𝐹 ∈ CRing → 𝑉 = (Base‘𝐿))
19 plusgid 17160 . . . . 5 +g = Slot (+g‘ndx)
20 plusgndx 17159 . . . . . 6 (+g‘ndx) = 2
21 2re 12227 . . . . . . . 8 2 ∈ ℝ
22 2lt6 12337 . . . . . . . 8 2 < 6
2321, 22ltneii 11268 . . . . . . 7 2 ≠ 6
2423, 9neeqtrri 3017 . . . . . 6 2 ≠ ( ·𝑠 ‘ndx)
2520, 24eqnetri 3014 . . . . 5 (+g‘ndx) ≠ ( ·𝑠 ‘ndx)
2619, 25setsnid 17081 . . . 4 (+g𝑅) = (+g‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
27 rmodislmod.a . . . 4 + = (+g𝑅)
2814fveq2i 6845 . . . 4 (+g𝐿) = (+g‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
2926, 27, 283eqtr4i 2774 . . 3 + = (+g𝐿)
3029a1i 11 . 2 (𝐹 ∈ CRing → + = (+g𝐿))
31 scaid 17196 . . . . 5 Scalar = Slot (Scalar‘ndx)
32 scandx 17195 . . . . . 6 (Scalar‘ndx) = 5
33 5re 12240 . . . . . . . 8 5 ∈ ℝ
34 5lt6 12334 . . . . . . . 8 5 < 6
3533, 34ltneii 11268 . . . . . . 7 5 ≠ 6
3635, 9neeqtrri 3017 . . . . . 6 5 ≠ ( ·𝑠 ‘ndx)
3732, 36eqnetri 3014 . . . . 5 (Scalar‘ndx) ≠ ( ·𝑠 ‘ndx)
3831, 37setsnid 17081 . . . 4 (Scalar‘𝑅) = (Scalar‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
39 rmodislmod.f . . . 4 𝐹 = (Scalar‘𝑅)
4014fveq2i 6845 . . . 4 (Scalar‘𝐿) = (Scalar‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
4138, 39, 403eqtr4i 2774 . . 3 𝐹 = (Scalar‘𝐿)
4241a1i 11 . 2 (𝐹 ∈ CRing → 𝐹 = (Scalar‘𝐿))
43 rmodislmod.r . . . . . 6 (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))
4443simp1i 1139 . . . . 5 𝑅 ∈ Grp
45 rmodislmod.k . . . . . . 7 𝐾 = (Base‘𝐹)
4645fvexi 6856 . . . . . 6 𝐾 ∈ V
471fvexi 6856 . . . . . 6 𝑉 ∈ V
48 rmodislmod.m . . . . . . 7 = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠))
4948mpoexg 8009 . . . . . 6 ((𝐾 ∈ V ∧ 𝑉 ∈ V) → ∈ V)
5046, 47, 49mp2an 690 . . . . 5 ∈ V
51 vscaid 17201 . . . . . 6 ·𝑠 = Slot ( ·𝑠 ‘ndx)
5251setsid 17080 . . . . 5 ((𝑅 ∈ Grp ∧ ∈ V) → = ( ·𝑠 ‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)))
5344, 50, 52mp2an 690 . . . 4 = ( ·𝑠 ‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩))
5415fveq2i 6845 . . . 4 ( ·𝑠 ‘(𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)) = ( ·𝑠𝐿)
5553, 54eqtri 2764 . . 3 = ( ·𝑠𝐿)
5655a1i 11 . 2 (𝐹 ∈ CRing → = ( ·𝑠𝐿))
5745a1i 11 . 2 (𝐹 ∈ CRing → 𝐾 = (Base‘𝐹))
58 rmodislmod.p . . 3 = (+g𝐹)
5958a1i 11 . 2 (𝐹 ∈ CRing → = (+g𝐹))
60 rmodislmod.t . . 3 × = (.r𝐹)
6160a1i 11 . 2 (𝐹 ∈ CRing → × = (.r𝐹))
62 rmodislmod.u . . 3 1 = (1r𝐹)
6362a1i 11 . 2 (𝐹 ∈ CRing → 1 = (1r𝐹))
64 crngring 19976 . 2 (𝐹 ∈ CRing → 𝐹 ∈ Ring)
651eqcomi 2745 . . . . . 6 (Base‘𝑅) = 𝑉
6665, 17eqtri 2764 . . . . 5 (Base‘𝑅) = (Base‘𝐿)
6726, 28eqtr4i 2767 . . . . 5 (+g𝑅) = (+g𝐿)
6866, 67grpprop 18766 . . . 4 (𝑅 ∈ Grp ↔ 𝐿 ∈ Grp)
6944, 68mpbi 229 . . 3 𝐿 ∈ Grp
7069a1i 11 . 2 (𝐹 ∈ CRing → 𝐿 ∈ Grp)
7148a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠)))
72 oveq12 7366 . . . . . 6 ((𝑣 = 𝑏𝑠 = 𝑎) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
7372ancoms 459 . . . . 5 ((𝑠 = 𝑎𝑣 = 𝑏) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
7473adantl 482 . . . 4 (((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) ∧ (𝑠 = 𝑎𝑣 = 𝑏)) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
75 simp2 1137 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → 𝑎𝐾)
76 simp3 1138 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → 𝑏𝑉)
77 ovexd 7392 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ V)
7871, 74, 75, 76, 77ovmpod 7507 . . 3 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑎 𝑏) = (𝑏 · 𝑎))
79 simpl1 1191 . . . . . . . 8 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 𝑟) ∈ 𝑉)
80792ralimi 3126 . . . . . . 7 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
81802ralimi 3126 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
82 ringgrp 19969 . . . . . . . . . 10 (𝐹 ∈ Ring → 𝐹 ∈ Grp)
8345grpbn0 18779 . . . . . . . . . 10 (𝐹 ∈ Grp → 𝐾 ≠ ∅)
8482, 83syl 17 . . . . . . . . 9 (𝐹 ∈ Ring → 𝐾 ≠ ∅)
85843ad2ant2 1134 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝐾 ≠ ∅)
8643, 85ax-mp 5 . . . . . . 7 𝐾 ≠ ∅
87 rspn0 4312 . . . . . . 7 (𝐾 ≠ ∅ → (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉))
8886, 87ax-mp 5 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
89 ralcom 3272 . . . . . . 7 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 ↔ ∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
901grpbn0 18779 . . . . . . . . . . 11 (𝑅 ∈ Grp → 𝑉 ≠ ∅)
91903ad2ant1 1133 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → 𝑉 ≠ ∅)
9243, 91ax-mp 5 . . . . . . . . 9 𝑉 ≠ ∅
93 rspn0 4312 . . . . . . . . 9 (𝑉 ≠ ∅ → (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉))
9492, 93ax-mp 5 . . . . . . . 8 (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉)
95 oveq2 7365 . . . . . . . . . . 11 (𝑟 = 𝑎 → (𝑤 · 𝑟) = (𝑤 · 𝑎))
9695eleq1d 2822 . . . . . . . . . 10 (𝑟 = 𝑎 → ((𝑤 · 𝑟) ∈ 𝑉 ↔ (𝑤 · 𝑎) ∈ 𝑉))
97 oveq1 7364 . . . . . . . . . . 11 (𝑤 = 𝑏 → (𝑤 · 𝑎) = (𝑏 · 𝑎))
9897eleq1d 2822 . . . . . . . . . 10 (𝑤 = 𝑏 → ((𝑤 · 𝑎) ∈ 𝑉 ↔ (𝑏 · 𝑎) ∈ 𝑉))
9996, 98rspc2v 3590 . . . . . . . . 9 ((𝑎𝐾𝑏𝑉) → (∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑏 · 𝑎) ∈ 𝑉))
100993adant1 1130 . . . . . . . 8 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (∀𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → (𝑏 · 𝑎) ∈ 𝑉))
10194, 100syl5com 31 . . . . . . 7 (∀𝑥𝑉𝑟𝐾𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
10289, 101sylbi 216 . . . . . 6 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 𝑟) ∈ 𝑉 → ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
10381, 88, 1023syl 18 . . . . 5 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
1041033ad2ant3 1135 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ 𝑉))
10543, 104ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑏 · 𝑎) ∈ 𝑉)
10678, 105eqeltrd 2838 . 2 ((𝐹 ∈ CRing ∧ 𝑎𝐾𝑏𝑉) → (𝑎 𝑏) ∈ 𝑉)
10748a1i 11 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠)))
108 oveq12 7366 . . . . . . . 8 ((𝑣 = (𝑏 + 𝑐) ∧ 𝑠 = 𝑎) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
109108ancoms 459 . . . . . . 7 ((𝑠 = 𝑎𝑣 = (𝑏 + 𝑐)) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
110109adantl 482 . . . . . 6 (((𝑎𝐾𝑏𝑉𝑐𝑉) ∧ (𝑠 = 𝑎𝑣 = (𝑏 + 𝑐))) → (𝑣 · 𝑠) = ((𝑏 + 𝑐) · 𝑎))
111 simp1 1136 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → 𝑎𝐾)
1121, 27grpcl 18756 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑏𝑉𝑐𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
11344, 112mp3an1 1448 . . . . . . 7 ((𝑏𝑉𝑐𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
1141133adant1 1130 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑏 + 𝑐) ∈ 𝑉)
115 ovexd 7392 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑏 + 𝑐) · 𝑎) ∈ V)
116107, 110, 111, 114, 115ovmpod 7507 . . . . 5 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑎 (𝑏 + 𝑐)) = ((𝑏 + 𝑐) · 𝑎))
117 simpl2 1192 . . . . . . . . . 10 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
1181172ralimi 3126 . . . . . . . . 9 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
1191182ralimi 3126 . . . . . . . 8 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
120 rspn0 4312 . . . . . . . . . 10 (𝐾 ≠ ∅ → (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ∀𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟))))
12186, 120ax-mp 5 . . . . . . . . 9 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ∀𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)))
122 oveq2 7365 . . . . . . . . . . . 12 (𝑟 = 𝑎 → ((𝑤 + 𝑥) · 𝑟) = ((𝑤 + 𝑥) · 𝑎))
123 oveq2 7365 . . . . . . . . . . . . 13 (𝑟 = 𝑎 → (𝑥 · 𝑟) = (𝑥 · 𝑎))
12495, 123oveq12d 7375 . . . . . . . . . . . 12 (𝑟 = 𝑎 → ((𝑤 · 𝑟) + (𝑥 · 𝑟)) = ((𝑤 · 𝑎) + (𝑥 · 𝑎)))
125122, 124eqeq12d 2752 . . . . . . . . . . 11 (𝑟 = 𝑎 → (((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ↔ ((𝑤 + 𝑥) · 𝑎) = ((𝑤 · 𝑎) + (𝑥 · 𝑎))))
126 oveq2 7365 . . . . . . . . . . . . 13 (𝑥 = 𝑐 → (𝑤 + 𝑥) = (𝑤 + 𝑐))
127126oveq1d 7372 . . . . . . . . . . . 12 (𝑥 = 𝑐 → ((𝑤 + 𝑥) · 𝑎) = ((𝑤 + 𝑐) · 𝑎))
128 oveq1 7364 . . . . . . . . . . . . 13 (𝑥 = 𝑐 → (𝑥 · 𝑎) = (𝑐 · 𝑎))
129128oveq2d 7373 . . . . . . . . . . . 12 (𝑥 = 𝑐 → ((𝑤 · 𝑎) + (𝑥 · 𝑎)) = ((𝑤 · 𝑎) + (𝑐 · 𝑎)))
130127, 129eqeq12d 2752 . . . . . . . . . . 11 (𝑥 = 𝑐 → (((𝑤 + 𝑥) · 𝑎) = ((𝑤 · 𝑎) + (𝑥 · 𝑎)) ↔ ((𝑤 + 𝑐) · 𝑎) = ((𝑤 · 𝑎) + (𝑐 · 𝑎))))
131 oveq1 7364 . . . . . . . . . . . . 13 (𝑤 = 𝑏 → (𝑤 + 𝑐) = (𝑏 + 𝑐))
132131oveq1d 7372 . . . . . . . . . . . 12 (𝑤 = 𝑏 → ((𝑤 + 𝑐) · 𝑎) = ((𝑏 + 𝑐) · 𝑎))
13397oveq1d 7372 . . . . . . . . . . . 12 (𝑤 = 𝑏 → ((𝑤 · 𝑎) + (𝑐 · 𝑎)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
134132, 133eqeq12d 2752 . . . . . . . . . . 11 (𝑤 = 𝑏 → (((𝑤 + 𝑐) · 𝑎) = ((𝑤 · 𝑎) + (𝑐 · 𝑎)) ↔ ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
135125, 130, 134rspc3v 3593 . . . . . . . . . 10 ((𝑎𝐾𝑐𝑉𝑏𝑉) → (∀𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
1361353com23 1126 . . . . . . . . 9 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (∀𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
137121, 136syl5com 31 . . . . . . . 8 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) → ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
138119, 137syl 17 . . . . . . 7 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
1391383ad2ant3 1135 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎))))
14043, 139ax-mp 5 . . . . 5 ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑏 + 𝑐) · 𝑎) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
141116, 140eqtrd 2776 . . . 4 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑎 (𝑏 + 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
142141adantl 482 . . 3 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝑉𝑐𝑉)) → (𝑎 (𝑏 + 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
14373adantl 482 . . . . . 6 (((𝑎𝐾𝑏𝑉𝑐𝑉) ∧ (𝑠 = 𝑎𝑣 = 𝑏)) → (𝑣 · 𝑠) = (𝑏 · 𝑎))
144 simp2 1137 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → 𝑏𝑉)
145 ovexd 7392 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑏 · 𝑎) ∈ V)
146107, 143, 111, 144, 145ovmpod 7507 . . . . 5 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑎 𝑏) = (𝑏 · 𝑎))
147 oveq12 7366 . . . . . . . 8 ((𝑣 = 𝑐𝑠 = 𝑎) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
148147ancoms 459 . . . . . . 7 ((𝑠 = 𝑎𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
149148adantl 482 . . . . . 6 (((𝑎𝐾𝑏𝑉𝑐𝑉) ∧ (𝑠 = 𝑎𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
150 simp3 1138 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → 𝑐𝑉)
151 ovexd 7392 . . . . . 6 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑐 · 𝑎) ∈ V)
152107, 149, 111, 150, 151ovmpod 7507 . . . . 5 ((𝑎𝐾𝑏𝑉𝑐𝑉) → (𝑎 𝑐) = (𝑐 · 𝑎))
153146, 152oveq12d 7375 . . . 4 ((𝑎𝐾𝑏𝑉𝑐𝑉) → ((𝑎 𝑏) + (𝑎 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
154153adantl 482 . . 3 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝑉𝑐𝑉)) → ((𝑎 𝑏) + (𝑎 𝑐)) = ((𝑏 · 𝑎) + (𝑐 · 𝑎)))
155142, 154eqtr4d 2779 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝑉𝑐𝑉)) → (𝑎 (𝑏 + 𝑐)) = ((𝑎 𝑏) + (𝑎 𝑐)))
156 simpl3 1193 . . . . . . . . 9 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
1571562ralimi 3126 . . . . . . . 8 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
1581572ralimi 3126 . . . . . . 7 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
159 ralrot3 3276 . . . . . . . 8 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ ∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
160 rspn0 4312 . . . . . . . . . 10 (𝑉 ≠ ∅ → (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))))
16192, 160ax-mp 5 . . . . . . . . 9 (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)))
162 oveq1 7364 . . . . . . . . . . . 12 (𝑞 = 𝑎 → (𝑞 𝑟) = (𝑎 𝑟))
163162oveq2d 7373 . . . . . . . . . . 11 (𝑞 = 𝑎 → (𝑤 · (𝑞 𝑟)) = (𝑤 · (𝑎 𝑟)))
164 oveq2 7365 . . . . . . . . . . . 12 (𝑞 = 𝑎 → (𝑤 · 𝑞) = (𝑤 · 𝑎))
165164oveq1d 7372 . . . . . . . . . . 11 (𝑞 = 𝑎 → ((𝑤 · 𝑞) + (𝑤 · 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟)))
166163, 165eqeq12d 2752 . . . . . . . . . 10 (𝑞 = 𝑎 → ((𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) ↔ (𝑤 · (𝑎 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟))))
167 oveq2 7365 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝑎 𝑟) = (𝑎 𝑏))
168167oveq2d 7373 . . . . . . . . . . 11 (𝑟 = 𝑏 → (𝑤 · (𝑎 𝑟)) = (𝑤 · (𝑎 𝑏)))
169 oveq2 7365 . . . . . . . . . . . 12 (𝑟 = 𝑏 → (𝑤 · 𝑟) = (𝑤 · 𝑏))
170169oveq2d 7373 . . . . . . . . . . 11 (𝑟 = 𝑏 → ((𝑤 · 𝑎) + (𝑤 · 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏)))
171168, 170eqeq12d 2752 . . . . . . . . . 10 (𝑟 = 𝑏 → ((𝑤 · (𝑎 𝑟)) = ((𝑤 · 𝑎) + (𝑤 · 𝑟)) ↔ (𝑤 · (𝑎 𝑏)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏))))
172 oveq1 7364 . . . . . . . . . . 11 (𝑤 = 𝑐 → (𝑤 · (𝑎 𝑏)) = (𝑐 · (𝑎 𝑏)))
173 oveq1 7364 . . . . . . . . . . . 12 (𝑤 = 𝑐 → (𝑤 · 𝑎) = (𝑐 · 𝑎))
174 oveq1 7364 . . . . . . . . . . . 12 (𝑤 = 𝑐 → (𝑤 · 𝑏) = (𝑐 · 𝑏))
175173, 174oveq12d 7375 . . . . . . . . . . 11 (𝑤 = 𝑐 → ((𝑤 · 𝑎) + (𝑤 · 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
176172, 175eqeq12d 2752 . . . . . . . . . 10 (𝑤 = 𝑐 → ((𝑤 · (𝑎 𝑏)) = ((𝑤 · 𝑎) + (𝑤 · 𝑏)) ↔ (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
177166, 171, 176rspc3v 3593 . . . . . . . . 9 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (∀𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
178161, 177syl5com 31 . . . . . . . 8 (∀𝑥𝑉𝑞𝐾𝑟𝐾𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
179159, 178sylbi 216 . . . . . . 7 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟)) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
180158, 179syl 17 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
1811803ad2ant3 1135 . . . . 5 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏))))
18243, 181ax-mp 5 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
18348a1i 11 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠)))
184 oveq12 7366 . . . . . . 7 ((𝑣 = 𝑐𝑠 = (𝑎 𝑏)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 𝑏)))
185184ancoms 459 . . . . . 6 ((𝑠 = (𝑎 𝑏) ∧ 𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · (𝑎 𝑏)))
186185adantl 482 . . . . 5 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = (𝑎 𝑏) ∧ 𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · (𝑎 𝑏)))
18745, 58grpcl 18756 . . . . . . . . . 10 ((𝐹 ∈ Grp ∧ 𝑎𝐾𝑏𝐾) → (𝑎 𝑏) ∈ 𝐾)
1881873expib 1122 . . . . . . . . 9 (𝐹 ∈ Grp → ((𝑎𝐾𝑏𝐾) → (𝑎 𝑏) ∈ 𝐾))
18982, 188syl 17 . . . . . . . 8 (𝐹 ∈ Ring → ((𝑎𝐾𝑏𝐾) → (𝑎 𝑏) ∈ 𝐾))
1901893ad2ant2 1134 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝑎𝐾𝑏𝐾) → (𝑎 𝑏) ∈ 𝐾))
19143, 190ax-mp 5 . . . . . 6 ((𝑎𝐾𝑏𝐾) → (𝑎 𝑏) ∈ 𝐾)
1921913adant3 1132 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 𝑏) ∈ 𝐾)
193 simp3 1138 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑐𝑉)
194 ovexd 7392 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · (𝑎 𝑏)) ∈ V)
195183, 186, 192, 193, 194ovmpod 7507 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑎 𝑏) 𝑐) = (𝑐 · (𝑎 𝑏)))
196148adantl 482 . . . . . 6 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = 𝑎𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑎))
197 simp1 1136 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑎𝐾)
198 ovexd 7392 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · 𝑎) ∈ V)
199183, 196, 197, 193, 198ovmpod 7507 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑎 𝑐) = (𝑐 · 𝑎))
200 oveq12 7366 . . . . . . . 8 ((𝑣 = 𝑐𝑠 = 𝑏) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
201200ancoms 459 . . . . . . 7 ((𝑠 = 𝑏𝑣 = 𝑐) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
202201adantl 482 . . . . . 6 (((𝑎𝐾𝑏𝐾𝑐𝑉) ∧ (𝑠 = 𝑏𝑣 = 𝑐)) → (𝑣 · 𝑠) = (𝑐 · 𝑏))
203 simp2 1137 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → 𝑏𝐾)
204 ovexd 7392 . . . . . 6 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑐 · 𝑏) ∈ V)
205183, 202, 203, 193, 204ovmpod 7507 . . . . 5 ((𝑎𝐾𝑏𝐾𝑐𝑉) → (𝑏 𝑐) = (𝑐 · 𝑏))
206199, 205oveq12d 7375 . . . 4 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑎 𝑐) + (𝑏 𝑐)) = ((𝑐 · 𝑎) + (𝑐 · 𝑏)))
207182, 195, 2063eqtr4d 2786 . . 3 ((𝑎𝐾𝑏𝐾𝑐𝑉) → ((𝑎 𝑏) 𝑐) = ((𝑎 𝑐) + (𝑏 𝑐)))
208207adantl 482 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑎 𝑏) 𝑐) = ((𝑎 𝑐) + (𝑏 𝑐)))
209 rmodislmod.s . . 3 · = ( ·𝑠𝑅)
2101, 27, 209, 39, 45, 58, 60, 62, 43, 48, 14rmodislmodlem 20389 . 2 ((𝐹 ∈ CRing ∧ (𝑎𝐾𝑏𝐾𝑐𝑉)) → ((𝑎 × 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
21148a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠)))
212 oveq12 7366 . . . . . 6 ((𝑣 = 𝑎𝑠 = 1 ) → (𝑣 · 𝑠) = (𝑎 · 1 ))
213212ancoms 459 . . . . 5 ((𝑠 = 1𝑣 = 𝑎) → (𝑣 · 𝑠) = (𝑎 · 1 ))
214213adantl 482 . . . 4 (((𝐹 ∈ CRing ∧ 𝑎𝑉) ∧ (𝑠 = 1𝑣 = 𝑎)) → (𝑣 · 𝑠) = (𝑎 · 1 ))
21545, 62ringidcl 19989 . . . . . 6 (𝐹 ∈ Ring → 1𝐾)
21664, 215syl 17 . . . . 5 (𝐹 ∈ CRing → 1𝐾)
217216adantr 481 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → 1𝐾)
218 simpr 485 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → 𝑎𝑉)
219 ovexd 7392 . . . 4 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) ∈ V)
220211, 214, 217, 218, 219ovmpod 7507 . . 3 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → ( 1 𝑎) = (𝑎 · 1 ))
221 simprr 771 . . . . . . . 8 ((((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → (𝑤 · 1 ) = 𝑤)
2222212ralimi 3126 . . . . . . 7 (∀𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤)
2232222ralimi 3126 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤)
224 rspn0 4312 . . . . . . 7 (𝐾 ≠ ∅ → (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤))
22586, 224ax-mp 5 . . . . . 6 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤)
226 rspn0 4312 . . . . . . . 8 (𝐾 ≠ ∅ → (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤))
22786, 226ax-mp 5 . . . . . . 7 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤)
228 rspn0 4312 . . . . . . . . 9 (𝑉 ≠ ∅ → (∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑤𝑉 (𝑤 · 1 ) = 𝑤))
22992, 228ax-mp 5 . . . . . . . 8 (∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ∀𝑤𝑉 (𝑤 · 1 ) = 𝑤)
230 oveq1 7364 . . . . . . . . . . 11 (𝑤 = 𝑎 → (𝑤 · 1 ) = (𝑎 · 1 ))
231 id 22 . . . . . . . . . . 11 (𝑤 = 𝑎𝑤 = 𝑎)
232230, 231eqeq12d 2752 . . . . . . . . . 10 (𝑤 = 𝑎 → ((𝑤 · 1 ) = 𝑤 ↔ (𝑎 · 1 ) = 𝑎))
233232rspcv 3577 . . . . . . . . 9 (𝑎𝑉 → (∀𝑤𝑉 (𝑤 · 1 ) = 𝑤 → (𝑎 · 1 ) = 𝑎))
234233adantl 482 . . . . . . . 8 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (∀𝑤𝑉 (𝑤 · 1 ) = 𝑤 → (𝑎 · 1 ) = 𝑎))
235229, 234syl5com 31 . . . . . . 7 (∀𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) = 𝑎))
236227, 235syl 17 . . . . . 6 (∀𝑟𝐾𝑥𝑉𝑤𝑉 (𝑤 · 1 ) = 𝑤 → ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) = 𝑎))
237223, 225, 2363syl 18 . . . . 5 (∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)) → ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) = 𝑎))
2382373ad2ant3 1135 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤))) → ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) = 𝑎))
23943, 238ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → (𝑎 · 1 ) = 𝑎)
240220, 239eqtrd 2776 . 2 ((𝐹 ∈ CRing ∧ 𝑎𝑉) → ( 1 𝑎) = 𝑎)
24118, 30, 42, 56, 57, 59, 61, 63, 64, 70, 106, 155, 208, 210, 240islmodd 20328 1 (𝐹 ∈ CRing → 𝐿 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  Vcvv 3445  c0 4282  cop 4592  cfv 6496  (class class class)co 7357  cmpo 7359  1c1 11052  2c2 12208  5c5 12211  6c6 12212   sSet csts 17035  ndxcnx 17065  Basecbs 17083  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  Grpcgrp 18748  1rcur 19913  Ringcrg 19964  CRingccrg 19965  LModclmod 20322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-plusg 17146  df-sca 17149  df-vsca 17150  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-cmn 19564  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-lmod 20324
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator