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

Theorem rmodislmod 20540
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 20473 of a left module, see also islmod 20475. (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 17147 . . . . . 6 Base = Slot (Baseβ€˜ndx)
3 vscandxnbasendx 17266 . . . . . . 7 ( ·𝑠 β€˜ndx) β‰  (Baseβ€˜ndx)
43necomi 2996 . . . . . 6 (Baseβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
52, 4setsnid 17142 . . . . 5 (Baseβ€˜π‘…) = (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
61, 5eqtri 2761 . . . 4 𝑉 = (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
7 rmodislmod.l . . . . . 6 𝐿 = (𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)
87eqcomi 2742 . . . . 5 (𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩) = 𝐿
98fveq2i 6895 . . . 4 (Baseβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)) = (Baseβ€˜πΏ)
106, 9eqtri 2761 . . 3 𝑉 = (Baseβ€˜πΏ)
1110a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝑉 = (Baseβ€˜πΏ))
12 plusgid 17224 . . . . 5 +g = Slot (+gβ€˜ndx)
13 vscandxnplusgndx 17267 . . . . . 6 ( ·𝑠 β€˜ndx) β‰  (+gβ€˜ndx)
1413necomi 2996 . . . . 5 (+gβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
1512, 14setsnid 17142 . . . 4 (+gβ€˜π‘…) = (+gβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
16 rmodislmod.a . . . 4 + = (+gβ€˜π‘…)
177fveq2i 6895 . . . 4 (+gβ€˜πΏ) = (+gβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
1815, 16, 173eqtr4i 2771 . . 3 + = (+gβ€˜πΏ)
1918a1i 11 . 2 (𝐹 ∈ CRing β†’ + = (+gβ€˜πΏ))
20 scaid 17260 . . . . 5 Scalar = Slot (Scalarβ€˜ndx)
21 vscandxnscandx 17269 . . . . . 6 ( ·𝑠 β€˜ndx) β‰  (Scalarβ€˜ndx)
2221necomi 2996 . . . . 5 (Scalarβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
2320, 22setsnid 17142 . . . 4 (Scalarβ€˜π‘…) = (Scalarβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
24 rmodislmod.f . . . 4 𝐹 = (Scalarβ€˜π‘…)
257fveq2i 6895 . . . 4 (Scalarβ€˜πΏ) = (Scalarβ€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
2623, 24, 253eqtr4i 2771 . . 3 𝐹 = (Scalarβ€˜πΏ)
2726a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝐹 = (Scalarβ€˜πΏ))
28 rmodislmod.r . . . . . 6 (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)))
2928simp1i 1140 . . . . 5 𝑅 ∈ Grp
30 rmodislmod.k . . . . . . 7 𝐾 = (Baseβ€˜πΉ)
3130fvexi 6906 . . . . . 6 𝐾 ∈ V
321fvexi 6906 . . . . . 6 𝑉 ∈ V
33 rmodislmod.m . . . . . . 7 βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠))
3433mpoexg 8063 . . . . . 6 ((𝐾 ∈ V ∧ 𝑉 ∈ V) β†’ βˆ— ∈ V)
3531, 32, 34mp2an 691 . . . . 5 βˆ— ∈ V
36 vscaid 17265 . . . . . 6 ·𝑠 = Slot ( ·𝑠 β€˜ndx)
3736setsid 17141 . . . . 5 ((𝑅 ∈ Grp ∧ βˆ— ∈ V) β†’ βˆ— = ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)))
3829, 35, 37mp2an 691 . . . 4 βˆ— = ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩))
398fveq2i 6895 . . . 4 ( ·𝑠 β€˜(𝑅 sSet ⟨( ·𝑠 β€˜ndx), βˆ— ⟩)) = ( ·𝑠 β€˜πΏ)
4038, 39eqtri 2761 . . 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 20068 . 2 (𝐹 ∈ CRing β†’ 𝐹 ∈ Ring)
501eqcomi 2742 . . . . . 6 (Baseβ€˜π‘…) = 𝑉
5150, 10eqtri 2761 . . . . 5 (Baseβ€˜π‘…) = (Baseβ€˜πΏ)
5215, 17eqtr4i 2764 . . . . 5 (+gβ€˜π‘…) = (+gβ€˜πΏ)
5351, 52grpprop 18838 . . . 4 (𝑅 ∈ Grp ↔ 𝐿 ∈ Grp)
5429, 53mpbi 229 . . 3 𝐿 ∈ Grp
5554a1i 11 . 2 (𝐹 ∈ CRing β†’ 𝐿 ∈ Grp)
5633a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
57 oveq12 7418 . . . . . 6 ((𝑣 = 𝑏 ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
5857ancoms 460 . . . . 5 ((𝑠 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
5958adantl 483 . . . 4 (((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
60 simp2 1138 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
61 simp3 1139 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ 𝑏 ∈ 𝑉)
62 ovexd 7444 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ V)
6356, 59, 60, 61, 62ovmpod 7560 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) = (𝑏 Β· π‘Ž))
64 simpl1 1192 . . . . . . . 8 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· π‘Ÿ) ∈ 𝑉)
65642ralimi 3124 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
66652ralimi 3124 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
67 ringgrp 20061 . . . . . . . . . 10 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
6830grpbn0 18851 . . . . . . . . . 10 (𝐹 ∈ Grp β†’ 𝐾 β‰  βˆ…)
6967, 68syl 17 . . . . . . . . 9 (𝐹 ∈ Ring β†’ 𝐾 β‰  βˆ…)
70693ad2ant2 1135 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝐾 β‰  βˆ…)
7128, 70ax-mp 5 . . . . . . 7 𝐾 β‰  βˆ…
72 rspn0 4353 . . . . . . 7 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
7371, 72ax-mp 5 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
74 ralcom 3287 . . . . . . 7 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
751grpbn0 18851 . . . . . . . . . . 11 (𝑅 ∈ Grp β†’ 𝑉 β‰  βˆ…)
76753ad2ant1 1134 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝑉 β‰  βˆ…)
7728, 76ax-mp 5 . . . . . . . . 9 𝑉 β‰  βˆ…
78 rspn0 4353 . . . . . . . . 9 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
7977, 78ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
80 oveq2 7417 . . . . . . . . . . 11 (π‘Ÿ = π‘Ž β†’ (𝑀 Β· π‘Ÿ) = (𝑀 Β· π‘Ž))
8180eleq1d 2819 . . . . . . . . . 10 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ (𝑀 Β· π‘Ž) ∈ 𝑉))
82 oveq1 7416 . . . . . . . . . . 11 (𝑀 = 𝑏 β†’ (𝑀 Β· π‘Ž) = (𝑏 Β· π‘Ž))
8382eleq1d 2819 . . . . . . . . . 10 (𝑀 = 𝑏 β†’ ((𝑀 Β· π‘Ž) ∈ 𝑉 ↔ (𝑏 Β· π‘Ž) ∈ 𝑉))
8481, 83rspc2v 3623 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
85843adant1 1131 . . . . . . . 8 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8679, 85syl5com 31 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8774, 86sylbi 216 . . . . . 6 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
8866, 73, 873syl 18 . . . . 5 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
89883ad2ant3 1136 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉))
9028, 89ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ 𝑉)
9163, 90eqeltrd 2834 . 2 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) ∈ 𝑉)
9233a1i 11 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
93 oveq12 7418 . . . . . . . 8 ((𝑣 = (𝑏 + 𝑐) ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
9493ancoms 460 . . . . . . 7 ((𝑠 = π‘Ž ∧ 𝑣 = (𝑏 + 𝑐)) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
9594adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = (𝑏 + 𝑐))) β†’ (𝑣 Β· 𝑠) = ((𝑏 + 𝑐) Β· π‘Ž))
96 simp1 1137 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
971, 16grpcl 18827 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
9829, 97mp3an1 1449 . . . . . . 7 ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
99983adant1 1131 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 + 𝑐) ∈ 𝑉)
100 ovexd 7444 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) ∈ V)
10192, 95, 96, 99, 100ovmpod 7560 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 + 𝑐) Β· π‘Ž))
102 simpl2 1193 . . . . . . . . . 10 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
1031022ralimi 3124 . . . . . . . . 9 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
1041032ralimi 3124 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
105 rspn0 4353 . . . . . . . . . 10 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ))))
10671, 105ax-mp 5 . . . . . . . . 9 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)))
107 oveq2 7417 . . . . . . . . . . . 12 (π‘Ÿ = π‘Ž β†’ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 + π‘₯) Β· π‘Ž))
108 oveq2 7417 . . . . . . . . . . . . 13 (π‘Ÿ = π‘Ž β†’ (π‘₯ Β· π‘Ÿ) = (π‘₯ Β· π‘Ž))
10980, 108oveq12d 7427 . . . . . . . . . . . 12 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)))
110107, 109eqeq12d 2749 . . . . . . . . . . 11 (π‘Ÿ = π‘Ž β†’ (((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ↔ ((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž))))
111 oveq2 7417 . . . . . . . . . . . . 13 (π‘₯ = 𝑐 β†’ (𝑀 + π‘₯) = (𝑀 + 𝑐))
112111oveq1d 7424 . . . . . . . . . . . 12 (π‘₯ = 𝑐 β†’ ((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 + 𝑐) Β· π‘Ž))
113 oveq1 7416 . . . . . . . . . . . . 13 (π‘₯ = 𝑐 β†’ (π‘₯ Β· π‘Ž) = (𝑐 Β· π‘Ž))
114113oveq2d 7425 . . . . . . . . . . . 12 (π‘₯ = 𝑐 β†’ ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
115112, 114eqeq12d 2749 . . . . . . . . . . 11 (π‘₯ = 𝑐 β†’ (((𝑀 + π‘₯) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (π‘₯ Β· π‘Ž)) ↔ ((𝑀 + 𝑐) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
116 oveq1 7416 . . . . . . . . . . . . 13 (𝑀 = 𝑏 β†’ (𝑀 + 𝑐) = (𝑏 + 𝑐))
117116oveq1d 7424 . . . . . . . . . . . 12 (𝑀 = 𝑏 β†’ ((𝑀 + 𝑐) Β· π‘Ž) = ((𝑏 + 𝑐) Β· π‘Ž))
11882oveq1d 7424 . . . . . . . . . . . 12 (𝑀 = 𝑏 β†’ ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
119117, 118eqeq12d 2749 . . . . . . . . . . 11 (𝑀 = 𝑏 β†’ (((𝑀 + 𝑐) Β· π‘Ž) = ((𝑀 Β· π‘Ž) + (𝑐 Β· π‘Ž)) ↔ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
120110, 115, 119rspc3v 3628 . . . . . . . . . 10 ((π‘Ž ∈ 𝐾 ∧ 𝑐 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
1211203com23 1127 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
122106, 121syl5com 31 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
123104, 122syl 17 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
1241233ad2ant3 1136 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž))))
12528, 124ax-mp 5 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑏 + 𝑐) Β· π‘Ž) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
126101, 125eqtrd 2773 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
127126adantl 483 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
12858adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑏 Β· π‘Ž))
129 simp2 1138 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ 𝑏 ∈ 𝑉)
130 ovexd 7444 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 Β· π‘Ž) ∈ V)
13192, 128, 96, 129, 130ovmpod 7560 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑏) = (𝑏 Β· π‘Ž))
132 oveq12 7418 . . . . . . . 8 ((𝑣 = 𝑐 ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
133132ancoms 460 . . . . . . 7 ((𝑠 = π‘Ž ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
134133adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
135 simp3 1139 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ 𝑐 ∈ 𝑉)
136 ovexd 7444 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· π‘Ž) ∈ V)
13792, 134, 96, 135, 136ovmpod 7560 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑐) = (𝑐 Β· π‘Ž))
138131, 137oveq12d 7427 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
139138adantl 483 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)) = ((𝑏 Β· π‘Ž) + (𝑐 Β· π‘Ž)))
140127, 139eqtr4d 2776 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) β†’ (π‘Ž βˆ— (𝑏 + 𝑐)) = ((π‘Ž βˆ— 𝑏) + (π‘Ž βˆ— 𝑐)))
141 simpl3 1194 . . . . . . . . 9 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
1421412ralimi 3124 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
1431422ralimi 3124 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
144 ralrot3 3291 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
145 rspn0 4353 . . . . . . . . . 10 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))))
14677, 145ax-mp 5 . . . . . . . . 9 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)))
147 oveq1 7416 . . . . . . . . . . . 12 (π‘ž = π‘Ž β†’ (π‘ž ⨣ π‘Ÿ) = (π‘Ž ⨣ π‘Ÿ))
148147oveq2d 7425 . . . . . . . . . . 11 (π‘ž = π‘Ž β†’ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)))
149 oveq2 7417 . . . . . . . . . . . 12 (π‘ž = π‘Ž β†’ (𝑀 Β· π‘ž) = (𝑀 Β· π‘Ž))
150149oveq1d 7424 . . . . . . . . . . 11 (π‘ž = π‘Ž β†’ ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)))
151148, 150eqeq12d 2749 . . . . . . . . . 10 (π‘ž = π‘Ž β†’ ((𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) ↔ (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ))))
152 oveq2 7417 . . . . . . . . . . . 12 (π‘Ÿ = 𝑏 β†’ (π‘Ž ⨣ π‘Ÿ) = (π‘Ž ⨣ 𝑏))
153152oveq2d 7425 . . . . . . . . . . 11 (π‘Ÿ = 𝑏 β†’ (𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = (𝑀 Β· (π‘Ž ⨣ 𝑏)))
154 oveq2 7417 . . . . . . . . . . . 12 (π‘Ÿ = 𝑏 β†’ (𝑀 Β· π‘Ÿ) = (𝑀 Β· 𝑏))
155154oveq2d 7425 . . . . . . . . . . 11 (π‘Ÿ = 𝑏 β†’ ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)))
156153, 155eqeq12d 2749 . . . . . . . . . 10 (π‘Ÿ = 𝑏 β†’ ((𝑀 Β· (π‘Ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· π‘Ÿ)) ↔ (𝑀 Β· (π‘Ž ⨣ 𝑏)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏))))
157 oveq1 7416 . . . . . . . . . . 11 (𝑀 = 𝑐 β†’ (𝑀 Β· (π‘Ž ⨣ 𝑏)) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
158 oveq1 7416 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ (𝑀 Β· π‘Ž) = (𝑐 Β· π‘Ž))
159 oveq1 7416 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ (𝑀 Β· 𝑏) = (𝑐 Β· 𝑏))
160158, 159oveq12d 7427 . . . . . . . . . . 11 (𝑀 = 𝑐 β†’ ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
161157, 160eqeq12d 2749 . . . . . . . . . 10 (𝑀 = 𝑐 β†’ ((𝑀 Β· (π‘Ž ⨣ 𝑏)) = ((𝑀 Β· π‘Ž) + (𝑀 Β· 𝑏)) ↔ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
162151, 156, 161rspc3v 3628 . . . . . . . . 9 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
163146, 162syl5com 31 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
164144, 163sylbi 216 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
165143, 164syl 17 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
1661653ad2ant3 1136 . . . . 5 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏))))
16728, 166ax-mp 5 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
16833a1i 11 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
169 oveq12 7418 . . . . . . 7 ((𝑣 = 𝑐 ∧ 𝑠 = (π‘Ž ⨣ 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
170169ancoms 460 . . . . . 6 ((𝑠 = (π‘Ž ⨣ 𝑏) ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
171170adantl 483 . . . . 5 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (π‘Ž ⨣ 𝑏) ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
17230, 43grpcl 18827 . . . . . . . . . 10 ((𝐹 ∈ Grp ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
1731723expib 1123 . . . . . . . . 9 (𝐹 ∈ Grp β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
17467, 173syl 17 . . . . . . . 8 (𝐹 ∈ Ring β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
1751743ad2ant2 1135 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾))
17628, 175ax-mp 5 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
1771763adant3 1133 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž ⨣ 𝑏) ∈ 𝐾)
178 simp3 1139 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑐 ∈ 𝑉)
179 ovexd 7444 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž ⨣ 𝑏)) ∈ V)
180168, 171, 177, 178, 179ovmpod 7560 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = (𝑐 Β· (π‘Ž ⨣ 𝑏)))
181133adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· π‘Ž))
182 simp1 1137 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
183 ovexd 7444 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· π‘Ž) ∈ V)
184168, 181, 182, 178, 183ovmpod 7560 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— 𝑐) = (𝑐 Β· π‘Ž))
185 oveq12 7418 . . . . . . . 8 ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
186185ancoms 460 . . . . . . 7 ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
187186adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
188 simp2 1138 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑏 ∈ 𝐾)
189 ovexd 7444 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ V)
190168, 187, 188, 178, 189ovmpod 7560 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 βˆ— 𝑐) = (𝑐 Β· 𝑏))
191184, 190oveq12d 7427 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)) = ((𝑐 Β· π‘Ž) + (𝑐 Β· 𝑏)))
192167, 180, 1913eqtr4d 2783 . . 3 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)))
193192adantl 483 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž ⨣ 𝑏) βˆ— 𝑐) = ((π‘Ž βˆ— 𝑐) + (𝑏 βˆ— 𝑐)))
194 rmodislmod.s . . 3 Β· = ( ·𝑠 β€˜π‘…)
1951, 16, 194, 24, 30, 43, 45, 47, 28, 33, 7rmodislmodlem 20539 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (π‘Ž βˆ— (𝑏 βˆ— 𝑐)))
19633a1i 11 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
197 oveq12 7418 . . . . . 6 ((𝑣 = π‘Ž ∧ 𝑠 = 1 ) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
198197ancoms 460 . . . . 5 ((𝑠 = 1 ∧ 𝑣 = π‘Ž) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
199198adantl 483 . . . 4 (((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) ∧ (𝑠 = 1 ∧ 𝑣 = π‘Ž)) β†’ (𝑣 Β· 𝑠) = (π‘Ž Β· 1 ))
20030, 47ringidcl 20083 . . . . . 6 (𝐹 ∈ Ring β†’ 1 ∈ 𝐾)
20149, 200syl 17 . . . . 5 (𝐹 ∈ CRing β†’ 1 ∈ 𝐾)
202201adantr 482 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ 1 ∈ 𝐾)
203 simpr 486 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ π‘Ž ∈ 𝑉)
204 ovexd 7444 . . . 4 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) ∈ V)
205196, 199, 202, 203, 204ovmpod 7560 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ ( 1 βˆ— π‘Ž) = (π‘Ž Β· 1 ))
206 simprr 772 . . . . . . . 8 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· 1 ) = 𝑀)
2072062ralimi 3124 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
2082072ralimi 3124 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
209 rspn0 4353 . . . . . . 7 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21071, 209ax-mp 5 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
211 rspn0 4353 . . . . . . . 8 (𝐾 β‰  βˆ… β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21271, 211ax-mp 5 . . . . . . 7 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
213 rspn0 4353 . . . . . . . . 9 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀))
21477, 213ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀)
215 oveq1 7416 . . . . . . . . . . 11 (𝑀 = π‘Ž β†’ (𝑀 Β· 1 ) = (π‘Ž Β· 1 ))
216 id 22 . . . . . . . . . . 11 (𝑀 = π‘Ž β†’ 𝑀 = π‘Ž)
217215, 216eqeq12d 2749 . . . . . . . . . 10 (𝑀 = π‘Ž β†’ ((𝑀 Β· 1 ) = 𝑀 ↔ (π‘Ž Β· 1 ) = π‘Ž))
218217rspcv 3609 . . . . . . . . 9 (π‘Ž ∈ 𝑉 β†’ (βˆ€π‘€ ∈ 𝑉 (𝑀 Β· 1 ) = 𝑀 β†’ (π‘Ž Β· 1 ) = π‘Ž))
219218adantl 483 . . . . . . . 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 1136 . . . 4 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž))
22428, 223ax-mp 5 . . 3 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ (π‘Ž Β· 1 ) = π‘Ž)
225205, 224eqtrd 2773 . 2 ((𝐹 ∈ CRing ∧ π‘Ž ∈ 𝑉) β†’ ( 1 βˆ— π‘Ž) = π‘Ž)
22611, 19, 27, 41, 42, 44, 46, 48, 49, 55, 91, 140, 193, 195, 225islmodd 20477 1 (𝐹 ∈ CRing β†’ 𝐿 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  Vcvv 3475  βˆ…c0 4323  βŸ¨cop 4635  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411   sSet csts 17096  ndxcnx 17126  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  Grpcgrp 18819  1rcur 20004  Ringcrg 20056  CRingccrg 20057  LModclmod 20471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-plusg 17210  df-sca 17213  df-vsca 17214  df-0g 17387  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-cmn 19650  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-lmod 20473
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator