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

Theorem rmodislmodlem 20532
Description: Lemma for rmodislmod 20533. This is the part of the proof of rmodislmod 20533 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.)
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
rmodislmodlem ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (π‘Ž βˆ— (𝑏 βˆ— 𝑐)))
Distinct variable groups:   Γ— ,π‘ž,π‘Ÿ,𝑀,π‘₯   Γ— ,𝑠,𝑣   Β· ,π‘ž,π‘Ÿ,𝑀,π‘₯   Β· ,𝑠,𝑣   𝐾,π‘ž,π‘Ÿ,π‘₯   𝐾,𝑠,𝑣   𝑉,π‘ž,π‘Ÿ,𝑀,π‘₯   𝑉,𝑠,𝑣   π‘Ÿ,π‘Ž,𝑀   𝑠,π‘Ž,𝑣   π‘ž,𝑏,π‘Ÿ,𝑀   𝑠,𝑏,𝑣   𝑠,𝑐,𝑣   𝑀,𝑐
Allowed substitution hints:   + (π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   ⨣ (π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   𝑅(π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   Β· (π‘Ž,𝑏,𝑐)   Γ— (π‘Ž,𝑏,𝑐)   1 (π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   𝐹(π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   βˆ— (π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   𝐾(𝑀,π‘Ž,𝑏,𝑐)   𝐿(π‘₯,𝑀,𝑣,𝑠,π‘Ÿ,π‘ž,π‘Ž,𝑏,𝑐)   𝑉(π‘Ž,𝑏,𝑐)

Proof of Theorem rmodislmodlem
StepHypRef Expression
1 rmodislmod.r . . . . 5 (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)))
2 simprl 770 . . . . . . . . 9 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ))
322ralimi 3124 . . . . . . . 8 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ))
432ralimi 3124 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ))
5 ralrot3 3291 . . . . . . . . 9 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ))
6 rmodislmod.v . . . . . . . . . . . . . 14 𝑉 = (Baseβ€˜π‘…)
76grpbn0 18848 . . . . . . . . . . . . 13 (𝑅 ∈ Grp β†’ 𝑉 β‰  βˆ…)
873ad2ant1 1134 . . . . . . . . . . . 12 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝑉 β‰  βˆ…)
91, 8ax-mp 5 . . . . . . . . . . 11 𝑉 β‰  βˆ…
10 rspn0 4352 . . . . . . . . . . 11 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ)))
119, 10ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ))
12 oveq1 7413 . . . . . . . . . . . . . 14 (π‘ž = 𝑏 β†’ (π‘ž Γ— π‘Ÿ) = (𝑏 Γ— π‘Ÿ))
1312oveq2d 7422 . . . . . . . . . . . . 13 (π‘ž = 𝑏 β†’ (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = (𝑀 Β· (𝑏 Γ— π‘Ÿ)))
14 oveq2 7414 . . . . . . . . . . . . . 14 (π‘ž = 𝑏 β†’ (𝑀 Β· π‘ž) = (𝑀 Β· 𝑏))
1514oveq1d 7421 . . . . . . . . . . . . 13 (π‘ž = 𝑏 β†’ ((𝑀 Β· π‘ž) Β· π‘Ÿ) = ((𝑀 Β· 𝑏) Β· π‘Ÿ))
1613, 15eqeq12d 2749 . . . . . . . . . . . 12 (π‘ž = 𝑏 β†’ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ↔ (𝑀 Β· (𝑏 Γ— π‘Ÿ)) = ((𝑀 Β· 𝑏) Β· π‘Ÿ)))
17 oveq2 7414 . . . . . . . . . . . . . 14 (π‘Ÿ = π‘Ž β†’ (𝑏 Γ— π‘Ÿ) = (𝑏 Γ— π‘Ž))
1817oveq2d 7422 . . . . . . . . . . . . 13 (π‘Ÿ = π‘Ž β†’ (𝑀 Β· (𝑏 Γ— π‘Ÿ)) = (𝑀 Β· (𝑏 Γ— π‘Ž)))
19 oveq2 7414 . . . . . . . . . . . . 13 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· 𝑏) Β· π‘Ÿ) = ((𝑀 Β· 𝑏) Β· π‘Ž))
2018, 19eqeq12d 2749 . . . . . . . . . . . 12 (π‘Ÿ = π‘Ž β†’ ((𝑀 Β· (𝑏 Γ— π‘Ÿ)) = ((𝑀 Β· 𝑏) Β· π‘Ÿ) ↔ (𝑀 Β· (𝑏 Γ— π‘Ž)) = ((𝑀 Β· 𝑏) Β· π‘Ž)))
21 oveq1 7413 . . . . . . . . . . . . 13 (𝑀 = 𝑐 β†’ (𝑀 Β· (𝑏 Γ— π‘Ž)) = (𝑐 Β· (𝑏 Γ— π‘Ž)))
22 oveq1 7413 . . . . . . . . . . . . . 14 (𝑀 = 𝑐 β†’ (𝑀 Β· 𝑏) = (𝑐 Β· 𝑏))
2322oveq1d 7421 . . . . . . . . . . . . 13 (𝑀 = 𝑐 β†’ ((𝑀 Β· 𝑏) Β· π‘Ž) = ((𝑐 Β· 𝑏) Β· π‘Ž))
2421, 23eqeq12d 2749 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ ((𝑀 Β· (𝑏 Γ— π‘Ž)) = ((𝑀 Β· 𝑏) Β· π‘Ž) ↔ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž)))
2516, 20, 24rspc3v 3627 . . . . . . . . . . 11 ((𝑏 ∈ 𝐾 ∧ π‘Ž ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž)))
26253com12 1124 . . . . . . . . . 10 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž)))
2711, 26syl5com 31 . . . . . . . . 9 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž)))
285, 27sylbi 216 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž)))
29 eqcom 2740 . . . . . . . 8 (((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž)) ↔ (𝑐 Β· (𝑏 Γ— π‘Ž)) = ((𝑐 Β· 𝑏) Β· π‘Ž))
3028, 29syl6ibr 252 . . . . . . 7 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž))))
314, 30syl 17 . . . . . 6 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž))))
32313ad2ant3 1136 . . . . 5 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž))))
331, 32ax-mp 5 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž)))
3433adantl 483 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (𝑏 Γ— π‘Ž)))
35 rmodislmod.k . . . . . . . . . 10 𝐾 = (Baseβ€˜πΉ)
36 rmodislmod.t . . . . . . . . . 10 Γ— = (.rβ€˜πΉ)
3735, 36crngcom 20068 . . . . . . . . 9 ((𝐹 ∈ CRing ∧ 𝑏 ∈ 𝐾 ∧ π‘Ž ∈ 𝐾) β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏))
38373expb 1121 . . . . . . . 8 ((𝐹 ∈ CRing ∧ (𝑏 ∈ 𝐾 ∧ π‘Ž ∈ 𝐾)) β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏))
3938expcom 415 . . . . . . 7 ((𝑏 ∈ 𝐾 ∧ π‘Ž ∈ 𝐾) β†’ (𝐹 ∈ CRing β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏)))
4039ancoms 460 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (𝐹 ∈ CRing β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏)))
41403adant3 1133 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝐹 ∈ CRing β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏)))
4241impcom 409 . . . 4 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ (𝑏 Γ— π‘Ž) = (π‘Ž Γ— 𝑏))
4342oveq2d 7422 . . 3 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ (𝑐 Β· (𝑏 Γ— π‘Ž)) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
4434, 43eqtrd 2773 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
45 rmodislmod.m . . . . . . 7 βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠))
4645a1i 11 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ βˆ— = (𝑠 ∈ 𝐾, 𝑣 ∈ 𝑉 ↦ (𝑣 Β· 𝑠)))
47 oveq12 7415 . . . . . . . 8 ((𝑣 = 𝑐 ∧ 𝑠 = 𝑏) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
4847ancoms 460 . . . . . . 7 ((𝑠 = 𝑏 ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
4948adantl 483 . . . . . 6 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = 𝑏 ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· 𝑏))
50 simp2 1138 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑏 ∈ 𝐾)
51 simp3 1139 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ 𝑐 ∈ 𝑉)
52 ovexd 7441 . . . . . 6 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ V)
5346, 49, 50, 51, 52ovmpod 7557 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑏 βˆ— 𝑐) = (𝑐 Β· 𝑏))
5453oveq2d 7422 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 βˆ— 𝑐)) = (π‘Ž βˆ— (𝑐 Β· 𝑏)))
55 oveq12 7415 . . . . . . 7 ((𝑣 = (𝑐 Β· 𝑏) ∧ 𝑠 = π‘Ž) β†’ (𝑣 Β· 𝑠) = ((𝑐 Β· 𝑏) Β· π‘Ž))
5655ancoms 460 . . . . . 6 ((𝑠 = π‘Ž ∧ 𝑣 = (𝑐 Β· 𝑏)) β†’ (𝑣 Β· 𝑠) = ((𝑐 Β· 𝑏) Β· π‘Ž))
5756adantl 483 . . . . 5 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = π‘Ž ∧ 𝑣 = (𝑐 Β· 𝑏))) β†’ (𝑣 Β· 𝑠) = ((𝑐 Β· 𝑏) Β· π‘Ž))
58 simp1 1137 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ π‘Ž ∈ 𝐾)
59 simpl1 1192 . . . . . . . . . . 11 ((((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ (𝑀 Β· π‘Ÿ) ∈ 𝑉)
60592ralimi 3124 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
61602ralimi 3124 . . . . . . . . 9 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
62 ringgrp 20055 . . . . . . . . . . . . 13 (𝐹 ∈ Ring β†’ 𝐹 ∈ Grp)
6335grpbn0 18848 . . . . . . . . . . . . 13 (𝐹 ∈ Grp β†’ 𝐾 β‰  βˆ…)
6462, 63syl 17 . . . . . . . . . . . 12 (𝐹 ∈ Ring β†’ 𝐾 β‰  βˆ…)
65643ad2ant2 1135 . . . . . . . . . . 11 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ 𝐾 β‰  βˆ…)
661, 65ax-mp 5 . . . . . . . . . 10 𝐾 β‰  βˆ…
67 rspn0 4352 . . . . . . . . . 10 (𝐾 β‰  βˆ… β†’ (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
6866, 67ax-mp 5 . . . . . . . . 9 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
69 ralcom 3287 . . . . . . . . . 10 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
70 rspn0 4352 . . . . . . . . . . . 12 (𝑉 β‰  βˆ… β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉))
719, 70ax-mp 5 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉)
72 oveq2 7414 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑏 β†’ (𝑀 Β· π‘Ÿ) = (𝑀 Β· 𝑏))
7372eleq1d 2819 . . . . . . . . . . . 12 (π‘Ÿ = 𝑏 β†’ ((𝑀 Β· π‘Ÿ) ∈ 𝑉 ↔ (𝑀 Β· 𝑏) ∈ 𝑉))
7422eleq1d 2819 . . . . . . . . . . . 12 (𝑀 = 𝑐 β†’ ((𝑀 Β· 𝑏) ∈ 𝑉 ↔ (𝑐 Β· 𝑏) ∈ 𝑉))
7573, 74rspc2v 3622 . . . . . . . . . . 11 ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ (𝑐 Β· 𝑏) ∈ 𝑉))
7671, 75syl5com 31 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉))
7769, 76sylbi 216 . . . . . . . . 9 (βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (𝑀 Β· π‘Ÿ) ∈ 𝑉 β†’ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉))
7861, 68, 773syl 18 . . . . . . . 8 (βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀)) β†’ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉))
79783ad2ant3 1136 . . . . . . 7 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉))
801, 79ax-mp 5 . . . . . 6 ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉)
81803adant1 1131 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· 𝑏) ∈ 𝑉)
82 ovexd 7441 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((𝑐 Β· 𝑏) Β· π‘Ž) ∈ V)
8346, 57, 58, 81, 82ovmpod 7557 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑐 Β· 𝑏)) = ((𝑐 Β· 𝑏) Β· π‘Ž))
8454, 83eqtrd 2773 . . 3 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž βˆ— (𝑏 βˆ— 𝑐)) = ((𝑐 Β· 𝑏) Β· π‘Ž))
8584adantl 483 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ (π‘Ž βˆ— (𝑏 βˆ— 𝑐)) = ((𝑐 Β· 𝑏) Β· π‘Ž))
86 oveq12 7415 . . . . . 6 ((𝑣 = 𝑐 ∧ 𝑠 = (π‘Ž Γ— 𝑏)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
8786ancoms 460 . . . . 5 ((𝑠 = (π‘Ž Γ— 𝑏) ∧ 𝑣 = 𝑐) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
8887adantl 483 . . . 4 (((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) ∧ (𝑠 = (π‘Ž Γ— 𝑏) ∧ 𝑣 = 𝑐)) β†’ (𝑣 Β· 𝑠) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
8935, 36ringcl 20067 . . . . . . . 8 ((𝐹 ∈ Ring ∧ π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž Γ— 𝑏) ∈ 𝐾)
90893expib 1123 . . . . . . 7 (𝐹 ∈ Ring β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž Γ— 𝑏) ∈ 𝐾))
91903ad2ant2 1135 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((𝑀 Β· π‘Ÿ) ∈ 𝑉 ∧ ((𝑀 + π‘₯) Β· π‘Ÿ) = ((𝑀 Β· π‘Ÿ) + (π‘₯ Β· π‘Ÿ)) ∧ (𝑀 Β· (π‘ž ⨣ π‘Ÿ)) = ((𝑀 Β· π‘ž) + (𝑀 Β· π‘Ÿ))) ∧ ((𝑀 Β· (π‘ž Γ— π‘Ÿ)) = ((𝑀 Β· π‘ž) Β· π‘Ÿ) ∧ (𝑀 Β· 1 ) = 𝑀))) β†’ ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž Γ— 𝑏) ∈ 𝐾))
921, 91ax-mp 5 . . . . 5 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) β†’ (π‘Ž Γ— 𝑏) ∈ 𝐾)
93923adant3 1133 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (π‘Ž Γ— 𝑏) ∈ 𝐾)
94 ovexd 7441 . . . 4 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ (𝑐 Β· (π‘Ž Γ— 𝑏)) ∈ V)
9546, 88, 93, 51, 94ovmpod 7557 . . 3 ((π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
9695adantl 483 . 2 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (𝑐 Β· (π‘Ž Γ— 𝑏)))
9744, 85, 963eqtr4rd 2784 1 ((𝐹 ∈ CRing ∧ (π‘Ž ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝑉)) β†’ ((π‘Ž Γ— 𝑏) βˆ— 𝑐) = (π‘Ž βˆ— (𝑏 βˆ— 𝑐)))
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 4322  βŸ¨cop 4634  β€˜cfv 6541  (class class class)co 7406   ∈ cmpo 7408   sSet csts 17093  ndxcnx 17123  Basecbs 17141  +gcplusg 17194  .rcmulr 17195  Scalarcsca 17197   ·𝑠 cvsca 17198  Grpcgrp 18816  1rcur 19999  Ringcrg 20050  CRingccrg 20051
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-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-0g 17384  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-grp 18819  df-cmn 19645  df-mgp 19983  df-ring 20052  df-cring 20053
This theorem is referenced by:  rmodislmod  20533  rmodislmodOLD  20534
  Copyright terms: Public domain W3C validator