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

Theorem rmodislmod 20684
Description: 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 20616 of a left module, see also islmod 20618. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)
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
rmodislmod (𝐹 ∈ CRing β†’ 𝐿 ∈ LMod)
Distinct variable groups:   Γ— ,π‘ž,π‘Ÿ,𝑀,π‘₯   Γ— ,𝑠,𝑣   Β· ,π‘ž,π‘Ÿ,𝑀,π‘₯   Β· ,𝑠,𝑣   𝐾,π‘ž,π‘Ÿ,π‘₯   𝐾,𝑠,𝑣   𝑉,π‘ž,π‘Ÿ,𝑀,π‘₯   𝑉,𝑠,𝑣   𝐹,𝑠,𝑣   1 ,𝑠,𝑣   1 ,π‘ž,π‘Ÿ,𝑀,π‘₯   + ,π‘ž,π‘Ÿ,𝑀,π‘₯   + ,𝑠,𝑣   ⨣ ,π‘ž,π‘Ÿ,𝑀,π‘₯   ⨣ ,𝑠,𝑣
Allowed substitution hints:   𝑅(π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž)   𝐹(π‘₯,𝑀,π‘Ÿ,π‘ž)   βˆ— (π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž)   𝐾(𝑀)   𝐿(π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž)

Proof of Theorem rmodislmod
Dummy variables π‘Ž 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rmodislmod.v . . . . 5 𝑉 = (Baseβ€˜π‘…)
2 baseid 17151 . . . . . 6 Base = Slot (Baseβ€˜ndx)
3 vscandxnbasendx 17270 . . . . . . 7 ( ·𝑠 β€˜ndx) β‰  (Baseβ€˜ndx)
43necomi 2993 . . . . . 6 (Baseβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
52, 4setsnid 17146 . . . . 5 (Baseβ€˜π‘…) = (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
61, 5eqtri 2758 . . . 4 𝑉 = (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
7 rmodislmod.l . . . . . 6 𝐿 = (𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)
87eqcomi 2739 . . . . 5 (𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩) = 𝐿
98fveq2i 6893 . . . 4 (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)) = (Baseβ€˜πΏ)
106, 9eqtri 2758 . . 3 𝑉 = (Baseβ€˜πΏ)
1110a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝑉 = (Baseβ€˜πΏ))
12 plusgid 17228 . . . . 5 +g = Slot (+gβ€˜ndx)
13 vscandxnplusgndx 17271 . . . . . 6 ( ·𝑠 β€˜ndx) β‰  (+gβ€˜ndx)
1413necomi 2993 . . . . 5 (+gβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
1512, 14setsnid 17146 . . . 4 (+gβ€˜π‘…) = (+gβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
16 rmodislmod.a . . . 4 + = (+gβ€˜π‘…)
177fveq2i 6893 . . . 4 (+gβ€˜πΏ) = (+gβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
1815, 16, 173eqtr4i 2768 . . 3 + = (+gβ€˜πΏ)
1918a1i 11 . 2 (𝐹 ∈ CRing β†’ + = (+gβ€˜πΏ))
20 scaid 17264 . . . . 5 Scalar = Slot (Scalarβ€˜ndx)
21 vscandxnscandx 17273 . . . . . 6 ( ·𝑠 β€˜ndx) β‰  (Scalarβ€˜ndx)
2221necomi 2993 . . . . 5 (Scalarβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
2320, 22setsnid 17146 . . . 4 (Scalarβ€˜π‘…) = (Scalarβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
24 rmodislmod.f . . . 4 𝐹 = (Scalarβ€˜π‘…)
257fveq2i 6893 . . . 4 (Scalarβ€˜πΏ) = (Scalarβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
2623, 24, 253eqtr4i 2768 . . 3 𝐹 = (Scalarβ€˜πΏ)
2726a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝐹 = (Scalarβ€˜πΏ))
28 rmodislmod.r . . . . . 6 (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)))
2928simp1i 1137 . . . . 5 𝑅 ∈ Grp
30 rmodislmod.k . . . . . . 7 𝐾 = (Baseβ€˜πΉ)
3130fvexi 6904 . . . . . 6 𝐾 ∈ V
321fvexi 6904 . . . . . 6 𝑉 ∈ V
33 rmodislmod.m . . . . . . 7 βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠))
3433mpoexg 8065 . . . . . 6 ((𝐾 ∈ V ∧ 𝑉 ∈ V) β†’ βˆ— ∈ V)
3531, 32, 34mp2an 688 . . . . 5 βˆ— ∈ V
36 vscaid 17269 . . . . . 6 ·𝑠 = Slot ( ·𝑠 β€˜ndx)
3736setsid 17145 . . . . 5 ((𝑅 ∈ Grp ∧ βˆ— ∈ V) β†’ βˆ— = ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)))
3829, 35, 37mp2an 688 . . . 4 βˆ— = ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
398fveq2i 6893 . . . 4 ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)) = ( ·𝑠 β€˜πΏ)
4038, 39eqtri 2758 . . 3 βˆ— = ( ·𝑠 β€˜πΏ)
4140a1i 11 . 2 (𝐹 ∈ CRing β†’ βˆ— = ( ·𝑠 β€˜πΏ))
4230a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝐾 = (Baseβ€˜πΉ))
43 rmodislmod.p . . 3 ⨣ = (+gβ€˜πΉ)
4443a1i 11 . 2 (𝐹 ∈ CRing β†’ ⨣ = (+gβ€˜πΉ))
45 rmodislmod.t . . 3 Γ— = (.rβ€˜πΉ)
4645a1i 11 . 2 (𝐹 ∈ CRing β†’ Γ— = (.rβ€˜πΉ))
47 rmodislmod.u . . 3 1 = (1rβ€˜πΉ)
4847a1i 11 . 2 (𝐹 ∈ CRing β†’ 1 = (1rβ€˜πΉ))
49 crngring 20139 . 2 (𝐹 ∈ CRing β†’ 𝐹 ∈ Ring)
501eqcomi 2739 . . . . . 6 (Baseβ€˜π‘…) = 𝑉
5150, 10eqtri 2758 . . . . 5 (Baseβ€˜π‘…) = (Baseβ€˜πΏ)
5215, 17eqtr4i 2761 . . . . 5 (+gβ€˜π‘…) = (+gβ€˜πΏ)
5351, 52grpprop 18874 . . . 4 (𝑅 ∈ Grp ↔ 𝐿 ∈ Grp)
5429, 53mpbi 229 . . 3 𝐿 ∈ Grp
5554a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝐿 ∈ Grp)
5633a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
57 oveq12 7420 . . . . . 6 ((𝑣 = 𝑏 ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
5857ancoms 457 . . . . 5 ((𝑠 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
5958adantl 480 . . . 4 (((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
60 simp2 1135 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
61 simp3 1136 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ 𝑏 ∈ 𝑉)
62 ovexd 7446 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ V)
6356, 59, 60, 61, 62ovmpod 7562 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) = (𝑏 Β· π‘Ž))
64 simpl1 1189 . . . . . . . 8 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· π‘Ÿ) ∈ 𝑉)
65642ralimi 3121 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
66652ralimi 3121 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
67 ringgrp 20132 . . . . . . . . . 10 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
6830grpbn0 18887 . . . . . . . . . 10 (𝐹 ∈ Grp β†’ 𝐾 β‰  βˆ…)
6967, 68syl 17 . . . . . . . . 9 (𝐹 ∈ Ring β†’ 𝐾 β‰  βˆ…)
70693ad2ant2 1132 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝐾 β‰  βˆ…)
7128, 70ax-mp 5 . . . . . . 7 𝐾 β‰  βˆ…
72 rspn0 4351 . . . . . . 7 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
7371, 72ax-mp 5 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
74 ralcom 3284 . . . . . . 7 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
751grpbn0 18887 . . . . . . . . . . 11 (𝑅 ∈ Grp β†’ 𝑉 β‰  βˆ…)
76753ad2ant1 1131 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝑉 β‰  βˆ…)
7728, 76ax-mp 5 . . . . . . . . 9 𝑉 β‰  βˆ…
78 rspn0 4351 . . . . . . . . 9 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
7977, 78ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
80 oveq2 7419 . . . . . . . . . . 11 (π‘Ÿ = π‘Ž β†’ (𝑀 Β· π‘Ÿ) = (𝑀 Β· π‘Ž))
8180eleq1d 2816 . . . . . . . . . 10 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ (𝑀 Β· π‘Ž) ∈ 𝑉))
82 oveq1 7418 . . . . . . . . . . 11 (𝑀 = 𝑏 β†’ (𝑀 Β· π‘Ž) = (𝑏 Β· π‘Ž))
8382eleq1d 2816 . . . . . . . . . 10 (𝑀 = 𝑏 β†’ ((𝑀 Β· π‘Ž) ∈ 𝑉 ↔ (𝑏 Β· π‘Ž) ∈ 𝑉))
8481, 83rspc2v 3621 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
85843adant1 1128 . . . . . . . 8 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8679, 85syl5com 31 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8774, 86sylbi 216 . . . . . 6 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8866, 73, 873syl 18 . . . . 5 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
89883ad2ant3 1133 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
9028, 89ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉)
9163, 90eqeltrd 2831 . 2 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) ∈ 𝑉)
9233a1i 11 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
93 oveq12 7420 . . . . . . . 8 ((𝑣 = (𝑏 + 𝑐) ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
9493ancoms 457 . . . . . . 7 ((𝑠 = π‘Ž ∧ 𝑣 = (𝑏 + 𝑐)) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
9594adantl 480 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = (𝑏 + 𝑐))) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
96 simp1 1134 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
971, 16grpcl 18863 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
9829, 97mp3an1 1446 . . . . . . 7 ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
99983adant1 1128 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
100 ovexd 7446 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) ∈ V)
10192, 95, 96, 99, 100ovmpod 7562 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 + 𝑐) Β· π‘Ž))
102 simpl2 1190 . . . . . . . . . 10 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
1031022ralimi 3121 . . . . . . . . 9 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
1041032ralimi 3121 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
105 rspn0 4351 . . . . . . . . . 10 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ))))
10671, 105ax-mp 5 . . . . . . . . 9 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
107 oveq2 7419 . . . . . . . . . . . 12 (π‘Ÿ = π‘Ž β†’ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 + π‘₯) Β· π‘Ž))
108 oveq2 7419 . . . . . . . . . . . . 13 (π‘Ÿ = π‘Ž β†’ (π‘₯ Β· π‘Ÿ) = (π‘₯ Β· π‘Ž))
10980, 108oveq12d 7429 . . . . . . . . . . . 12 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)))
110107, 109eqeq12d 2746 . . . . . . . . . . 11 (π‘Ÿ = π‘Ž β†’ (((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ↔ ((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž))))
111 oveq2 7419 . . . . . . . . . . . . 13 (π‘₯ = 𝑐 β†’ (𝑀 + π‘₯) = (𝑀 + 𝑐))
112111oveq1d 7426 . . . . . . . . . . . 12 (π‘₯ = 𝑐 β†’ ((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 + 𝑐) Β· π‘Ž))
113 oveq1 7418 . . . . . . . . . . . . 13 (π‘₯ = 𝑐 β†’ (π‘₯ Β· π‘Ž) = (𝑐 Β· π‘Ž))
114113oveq2d 7427 . . . . . . . . . . . 12 (π‘₯ = 𝑐 β†’ ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
115112, 114eqeq12d 2746 . . . . . . . . . . 11 (π‘₯ = 𝑐 β†’ (((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)) ↔ ((𝑀 + 𝑐) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
116 oveq1 7418 . . . . . . . . . . . . 13 (𝑀 = 𝑏 β†’ (𝑀 + 𝑐) = (𝑏 + 𝑐))
117116oveq1d 7426 . . . . . . . . . . . 12 (𝑀 = 𝑏 β†’ ((𝑀 + 𝑐) Β· π‘Ž) = ((𝑏 + 𝑐) Β· π‘Ž))
11882oveq1d 7426 . . . . . . . . . . . 12 (𝑀 = 𝑏 β†’ ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
119117, 118eqeq12d 2746 . . . . . . . . . . 11 (𝑀 = 𝑏 β†’ (((𝑀 + 𝑐) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)) ↔ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
120110, 115, 119rspc3v 3626 . . . . . . . . . 10 ((π‘Ž ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
1211203com23 1124 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
122106, 121syl5com 31 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
123104, 122syl 17 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
1241233ad2ant3 1133 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
12528, 124ax-mp 5 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
126101, 125eqtrd 2770 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
127126adantl 480 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
12858adantl 480 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
129 simp2 1135 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ 𝑏 ∈ 𝑉)
130 ovexd 7446 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ V)
13192, 128, 96, 129, 130ovmpod 7562 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) = (𝑏 Β· π‘Ž))
132 oveq12 7420 . . . . . . . 8 ((𝑣 = 𝑐 ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
133132ancoms 457 . . . . . . 7 ((𝑠 = π‘Ž ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
134133adantl 480 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
135 simp3 1136 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ 𝑐 ∈ 𝑉)
136 ovexd 7446 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· π‘Ž) ∈ V)
13792, 134, 96, 135, 136ovmpod 7562 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑐) = (𝑐 Β· π‘Ž))
138131, 137oveq12d 7429 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
139138adantl 480 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
140127, 139eqtr4d 2773 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)))
141 simpl3 1191 . . . . . . . . 9 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
1421412ralimi 3121 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
1431422ralimi 3121 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
144 ralrot3 3288 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
145 rspn0 4351 . . . . . . . . . 10 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))))
14677, 145ax-mp 5 . . . . . . . . 9 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
147 oveq1 7418 . . . . . . . . . . . 12 (π‘ž = π‘Ž β†’ (π‘ž ⨣ π‘Ÿ) = (π‘Ž ⨣ π‘Ÿ))
148147oveq2d 7427 . . . . . . . . . . 11 (π‘ž = π‘Ž β†’ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)))
149 oveq2 7419 . . . . . . . . . . . 12 (π‘ž = π‘Ž β†’ (𝑀 Β· π‘ž) = (𝑀 Β· π‘Ž))
150149oveq1d 7426 . . . . . . . . . . 11 (π‘ž = π‘Ž β†’ ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)))
151148, 150eqeq12d 2746 . . . . . . . . . 10 (π‘ž = π‘Ž β†’ ((𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) ↔ (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ))))
152 oveq2 7419 . . . . . . . . . . . 12 (π‘Ÿ = 𝑏 β†’ (π‘Ž ⨣ π‘Ÿ) = (π‘Ž ⨣ 𝑏))
153152oveq2d 7427 . . . . . . . . . . 11 (π‘Ÿ = 𝑏 β†’ (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = (𝑀 Β· (π‘Ž ⨣ 𝑏)))
154 oveq2 7419 . . . . . . . . . . . 12 (π‘Ÿ = 𝑏 β†’ (𝑀 Β· π‘Ÿ) = (𝑀 Β· 𝑏))
155154oveq2d 7427 . . . . . . . . . . 11 (π‘Ÿ = 𝑏 β†’ ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)))
156153, 155eqeq12d 2746 . . . . . . . . . 10 (π‘Ÿ = 𝑏 β†’ ((𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)) ↔ (𝑀 Β· (π‘Ž ⨣ 𝑏)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏))))
157 oveq1 7418 . . . . . . . . . . 11 (𝑀 = 𝑐 β†’ (𝑀 Β· (π‘Ž ⨣ 𝑏)) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
158 oveq1 7418 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ (𝑀 Β· π‘Ž) = (𝑐 Β· π‘Ž))
159 oveq1 7418 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ (𝑀 Β· 𝑏) = (𝑐 Β· 𝑏))
160158, 159oveq12d 7429 . . . . . . . . . . 11 (𝑀 = 𝑐 β†’ ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
161157, 160eqeq12d 2746 . . . . . . . . . 10 (𝑀 = 𝑐 β†’ ((𝑀 Β· (π‘Ž ⨣ 𝑏)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)) ↔ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
162151, 156, 161rspc3v 3626 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
163146, 162syl5com 31 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
164144, 163sylbi 216 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
165143, 164syl 17 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
1661653ad2ant3 1133 . . . . 5 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
16728, 166ax-mp 5 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
16833a1i 11 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
169 oveq12 7420 . . . . . . 7 ((𝑣 = 𝑐 ∧ 𝑠 = (π‘Ž ⨣ 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
170169ancoms 457 . . . . . 6 ((𝑠 = (π‘Ž ⨣ 𝑏) ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
171170adantl 480 . . . . 5 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (π‘Ž ⨣ 𝑏) ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
17230, 43grpcl 18863 . . . . . . . . . 10 ((𝐹 ∈ Grp ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
1731723expib 1120 . . . . . . . . 9 (𝐹 ∈ Grp β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
17467, 173syl 17 . . . . . . . 8 (𝐹 ∈ Ring β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
1751743ad2ant2 1132 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
17628, 175ax-mp 5 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
1771763adant3 1130 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
178 simp3 1136 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑐 ∈ 𝑉)
179 ovexd 7446 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) ∈ V)
180168, 171, 177, 178, 179ovmpod 7562 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
181133adantl 480 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
182 simp1 1134 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
183 ovexd 7446 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· π‘Ž) ∈ V)
184168, 181, 182, 178, 183ovmpod 7562 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑐) = (𝑐 Β· π‘Ž))
185 oveq12 7420 . . . . . . . 8 ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
186185ancoms 457 . . . . . . 7 ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
187186adantl 480 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
188 simp2 1135 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑏 ∈ 𝐾)
189 ovexd 7446 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ V)
190168, 187, 188, 178, 189ovmpod 7562 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 βˆ— 𝑐) = (𝑐 Β· 𝑏))
191184, 190oveq12d 7429 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
192167, 180, 1913eqtr4d 2780 . . 3 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)))
193192adantl 480 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)))
194 rmodislmod.s . . 3 Β· = ( ·𝑠 β€˜π‘…)
1951, 16, 194, 24, 30, 43, 45, 47, 28, 33, 7rmodislmodlem 20683 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (π‘Ž βˆ— (𝑏 βˆ— 𝑐)))
19633a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
197 oveq12 7420 . . . . . 6 ((𝑣 = π‘Ž ∧ 𝑠 = 1 ) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
198197ancoms 457 . . . . 5 ((𝑠 = 1 ∧ 𝑣 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
199198adantl 480 . . . 4 (((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) ∧ (𝑠 = 1 ∧ 𝑣 = π‘Ž)) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
20030, 47ringidcl 20154 . . . . . 6 (𝐹 ∈ Ring β†’ 1 ∈ 𝐾)
20149, 200syl 17 . . . . 5 (𝐹 ∈ CRing β†’ 1 ∈ 𝐾)
202201adantr 479 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ 1 ∈ 𝐾)
203 simpr 483 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ π‘Ž ∈ 𝑉)
204 ovexd 7446 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) ∈ V)
205196, 199, 202, 203, 204ovmpod 7562 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ ( 1 βˆ— π‘Ž) = (π‘Ž Β· 1 ))
206 simprr 769 . . . . . . . 8 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· 1 ) = 𝑀)
2072062ralimi 3121 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
2082072ralimi 3121 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
209 rspn0 4351 . . . . . . 7 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21071, 209ax-mp 5 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
211 rspn0 4351 . . . . . . . 8 (𝐾 β‰  βˆ… β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21271, 211ax-mp 5 . . . . . . 7 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
213 rspn0 4351 . . . . . . . . 9 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21477, 213ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
215 oveq1 7418 . . . . . . . . . . 11 (𝑀 = π‘Ž β†’ (𝑀 Β· 1 ) = (π‘Ž Β· 1 ))
216 id 22 . . . . . . . . . . 11 (𝑀 = π‘Ž β†’ 𝑀 = π‘Ž)
217215, 216eqeq12d 2746 . . . . . . . . . 10 (𝑀 = π‘Ž β†’ ((𝑀 Β· 1 ) = 𝑀 ↔ (π‘Ž Β· 1 ) = π‘Ž))
218217rspcv 3607 . . . . . . . . 9 (π‘Ž ∈ 𝑉 β†’ (βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ (π‘Ž Β· 1 ) = π‘Ž))
219218adantl 480 . . . . . . . 8 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ (π‘Ž Β· 1 ) = π‘Ž))
220214, 219syl5com 31 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž))
221212, 220syl 17 . . . . . 6 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž))
222208, 210, 2213syl 18 . . . . 5 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž))
2232223ad2ant3 1133 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž))
22428, 223ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž)
225205, 224eqtrd 2770 . 2 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ ( 1 βˆ— π‘Ž) = π‘Ž)
22611, 19, 27, 41, 42, 44, 46, 48, 49, 55, 91, 140, 193, 195, 225islmodd 20620 1 (𝐹 ∈ CRing β†’ 𝐿 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  Vcvv 3472  βˆ…c0 4321  βŸ¨cop 4633  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413   sSet csts 17100  ndxcnx 17130  Basecbs 17148  +gcplusg 17201  .rcmulr 17202  Scalarcsca 17204   ·𝑠 cvsca 17205  Grpcgrp 18855  1rcur 20075  Ringcrg 20127  CRingccrg 20128  LModclmod 20614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-plusg 17214  df-sca 17217  df-vsca 17218  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858  df-cmn 19691  df-mgp 20029  df-ur 20076  df-ring 20129  df-cring 20130  df-lmod 20616
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator