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

Theorem islmod 20475
Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
islmod.v 𝑉 = (Baseβ€˜π‘Š)
islmod.a + = (+gβ€˜π‘Š)
islmod.s Β· = ( ·𝑠 β€˜π‘Š)
islmod.f 𝐹 = (Scalarβ€˜π‘Š)
islmod.k 𝐾 = (Baseβ€˜πΉ)
islmod.p ⨣ = (+gβ€˜πΉ)
islmod.t Γ— = (.rβ€˜πΉ)
islmod.u 1 = (1rβ€˜πΉ)
Assertion
Ref Expression
islmod (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
Distinct variable groups:   π‘Ÿ,π‘ž,𝑀,π‘₯,𝐹   𝐾,π‘ž,π‘Ÿ,𝑀,π‘₯   ⨣ ,π‘ž,π‘Ÿ,𝑀,π‘₯   𝑉,π‘ž,π‘Ÿ,𝑀,π‘₯   + ,π‘ž,π‘Ÿ,𝑀,π‘₯   1 ,π‘ž,π‘Ÿ,𝑀,π‘₯   Γ— ,π‘ž,π‘Ÿ,𝑀,π‘₯   Β· ,π‘ž,π‘Ÿ,𝑀,π‘₯
Allowed substitution hints:   π‘Š(π‘₯,𝑀,π‘Ÿ,π‘ž)

Proof of Theorem islmod
Dummy variables 𝑓 π‘Ž 𝑔 π‘˜ 𝑝 𝑠 𝑣 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6892 . . . . . 6 (𝑔 = π‘Š β†’ (Baseβ€˜π‘”) = (Baseβ€˜π‘Š))
2 islmod.v . . . . . 6 𝑉 = (Baseβ€˜π‘Š)
31, 2eqtr4di 2791 . . . . 5 (𝑔 = π‘Š β†’ (Baseβ€˜π‘”) = 𝑉)
4 fveq2 6892 . . . . . . 7 (𝑔 = π‘Š β†’ (+gβ€˜π‘”) = (+gβ€˜π‘Š))
5 islmod.a . . . . . . 7 + = (+gβ€˜π‘Š)
64, 5eqtr4di 2791 . . . . . 6 (𝑔 = π‘Š β†’ (+gβ€˜π‘”) = + )
7 fveq2 6892 . . . . . . . 8 (𝑔 = π‘Š β†’ (Scalarβ€˜π‘”) = (Scalarβ€˜π‘Š))
8 islmod.f . . . . . . . 8 𝐹 = (Scalarβ€˜π‘Š)
97, 8eqtr4di 2791 . . . . . . 7 (𝑔 = π‘Š β†’ (Scalarβ€˜π‘”) = 𝐹)
10 fveq2 6892 . . . . . . . . 9 (𝑔 = π‘Š β†’ ( ·𝑠 β€˜π‘”) = ( ·𝑠 β€˜π‘Š))
11 islmod.s . . . . . . . . 9 Β· = ( ·𝑠 β€˜π‘Š)
1210, 11eqtr4di 2791 . . . . . . . 8 (𝑔 = π‘Š β†’ ( ·𝑠 β€˜π‘”) = Β· )
1312sbceq1d 3783 . . . . . . 7 (𝑔 = π‘Š β†’ ([( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
149, 13sbceqbid 3785 . . . . . 6 (𝑔 = π‘Š β†’ ([(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [𝐹 / 𝑓][ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
156, 14sbceqbid 3785 . . . . 5 (𝑔 = π‘Š β†’ ([(+gβ€˜π‘”) / π‘Ž][(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ + / π‘Ž][𝐹 / 𝑓][ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
163, 15sbceqbid 3785 . . . 4 (𝑔 = π‘Š β†’ ([(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [𝑉 / 𝑣][ + / π‘Ž][𝐹 / 𝑓][ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
172fvexi 6906 . . . . . 6 𝑉 ∈ V
185fvexi 6906 . . . . . 6 + ∈ V
198fvexi 6906 . . . . . 6 𝐹 ∈ V
20 simp3 1139 . . . . . . . . . 10 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ 𝑓 = 𝐹)
2120fveq2d 6896 . . . . . . . . 9 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (Baseβ€˜π‘“) = (Baseβ€˜πΉ))
22 islmod.k . . . . . . . . 9 𝐾 = (Baseβ€˜πΉ)
2321, 22eqtr4di 2791 . . . . . . . 8 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (Baseβ€˜π‘“) = 𝐾)
2420fveq2d 6896 . . . . . . . . . 10 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (+gβ€˜π‘“) = (+gβ€˜πΉ))
25 islmod.p . . . . . . . . . 10 ⨣ = (+gβ€˜πΉ)
2624, 25eqtr4di 2791 . . . . . . . . 9 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (+gβ€˜π‘“) = ⨣ )
2720fveq2d 6896 . . . . . . . . . . . 12 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (.rβ€˜π‘“) = (.rβ€˜πΉ))
28 islmod.t . . . . . . . . . . . 12 Γ— = (.rβ€˜πΉ)
2927, 28eqtr4di 2791 . . . . . . . . . . 11 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (.rβ€˜π‘“) = Γ— )
3029sbceq1d 3783 . . . . . . . . . 10 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ Γ— / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
3128fvexi 6906 . . . . . . . . . . . 12 Γ— ∈ V
32 oveq 7415 . . . . . . . . . . . . . . . . . . 19 (𝑑 = Γ— β†’ (π‘žπ‘‘π‘Ÿ) = (π‘ž Γ— π‘Ÿ))
3332oveq1d 7424 . . . . . . . . . . . . . . . . . 18 (𝑑 = Γ— β†’ ((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = ((π‘ž Γ— π‘Ÿ)𝑠𝑀))
3433eqeq1d 2735 . . . . . . . . . . . . . . . . 17 (𝑑 = Γ— β†’ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ↔ ((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€))))
3534anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑑 = Γ— β†’ ((((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀) ↔ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))
3635anbi2d 630 . . . . . . . . . . . . . . 15 (𝑑 = Γ— β†’ ((((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))))
37362ralbidv 3219 . . . . . . . . . . . . . 14 (𝑑 = Γ— β†’ (βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))))
38372ralbidv 3219 . . . . . . . . . . . . 13 (𝑑 = Γ— β†’ (βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))))
3938anbi2d 630 . . . . . . . . . . . 12 (𝑑 = Γ— β†’ ((𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))))
4031, 39sbcie 3821 . . . . . . . . . . 11 ([ Γ— / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))))
4120eleq1d 2819 . . . . . . . . . . . 12 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (𝑓 ∈ Ring ↔ 𝐹 ∈ Ring))
42 simp1 1137 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ 𝑣 = 𝑉)
4342eleq2d 2820 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((π‘Ÿπ‘ π‘€) ∈ 𝑣 ↔ (π‘Ÿπ‘ π‘€) ∈ 𝑉))
44 simp2 1138 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ π‘Ž = + )
4544oveqd 7426 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (π‘€π‘Žπ‘₯) = (𝑀 + π‘₯))
4645oveq2d 7425 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = (π‘Ÿπ‘ (𝑀 + π‘₯)))
4744oveqd 7426 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)))
4846, 47eqeq12d 2749 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ↔ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯))))
4944oveqd 7426 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€)))
5049eqeq2d 2744 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)) ↔ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))))
5143, 48, 503anbi123d 1437 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ↔ ((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€)))))
5220fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (1rβ€˜π‘“) = (1rβ€˜πΉ))
53 islmod.u . . . . . . . . . . . . . . . . . . . 20 1 = (1rβ€˜πΉ)
5452, 53eqtr4di 2791 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (1rβ€˜π‘“) = 1 )
5554oveq1d 7424 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((1rβ€˜π‘“)𝑠𝑀) = ( 1 𝑠𝑀))
5655eqeq1d 2735 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ↔ ( 1 𝑠𝑀) = 𝑀))
5756anbi2d 630 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀) ↔ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))
5851, 57anbi12d 632 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))))
5942, 58raleqbidv 3343 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))))
6042, 59raleqbidv 3343 . . . . . . . . . . . . 13 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))))
61602ralbidv 3219 . . . . . . . . . . . 12 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ (βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)) ↔ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))))
6241, 61anbi12d 632 . . . . . . . . . . 11 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ((𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6340, 62bitrid 283 . . . . . . . . . 10 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([ Γ— / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6430, 63bitrd 279 . . . . . . . . 9 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6526, 64sbceqbid 3785 . . . . . . . 8 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ ⨣ / 𝑝](𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6623, 65sbceqbid 3785 . . . . . . 7 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [𝐾 / π‘˜][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6766sbcbidv 3837 . . . . . 6 ((𝑣 = 𝑉 ∧ π‘Ž = + ∧ 𝑓 = 𝐹) β†’ ([ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ Β· / 𝑠][𝐾 / π‘˜][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)))))
6817, 18, 19, 67sbc3ie 3864 . . . . 5 ([𝑉 / 𝑣][ + / π‘Ž][𝐹 / 𝑓][ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ [ Β· / 𝑠][𝐾 / π‘˜][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))))
6911fvexi 6906 . . . . . 6 Β· ∈ V
7022fvexi 6906 . . . . . 6 𝐾 ∈ V
7125fvexi 6906 . . . . . 6 ⨣ ∈ V
72 simp2 1138 . . . . . . . 8 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ π‘˜ = 𝐾)
73 simp1 1137 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ 𝑠 = Β· )
7473oveqd 7426 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘Ÿπ‘ π‘€) = (π‘Ÿ Β· 𝑀))
7574eleq1d 2819 . . . . . . . . . . . 12 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘Ÿπ‘ π‘€) ∈ 𝑉 ↔ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
7673oveqd 7426 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘Ÿπ‘ (𝑀 + π‘₯)) = (π‘Ÿ Β· (𝑀 + π‘₯)))
7773oveqd 7426 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘Ÿπ‘ π‘₯) = (π‘Ÿ Β· π‘₯))
7874, 77oveq12d 7427 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)))
7976, 78eqeq12d 2749 . . . . . . . . . . . 12 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ↔ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯))))
80 simp3 1139 . . . . . . . . . . . . . . . 16 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ 𝑝 = ⨣ )
8180oveqd 7426 . . . . . . . . . . . . . . 15 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘žπ‘π‘Ÿ) = (π‘ž ⨣ π‘Ÿ))
8281oveq1d 7424 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘ž ⨣ π‘Ÿ)𝑠𝑀))
8373oveqd 7426 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘ž ⨣ π‘Ÿ)𝑠𝑀) = ((π‘ž ⨣ π‘Ÿ) Β· 𝑀))
8482, 83eqtrd 2773 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘ž ⨣ π‘Ÿ) Β· 𝑀))
8573oveqd 7426 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘žπ‘ π‘€) = (π‘ž Β· 𝑀))
8685, 74oveq12d 7427 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€)) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
8784, 86eqeq12d 2749 . . . . . . . . . . . 12 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€)) ↔ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
8875, 79, 873anbi123d 1437 . . . . . . . . . . 11 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ↔ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)))))
8973oveqd 7426 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((π‘ž Γ— π‘Ÿ)𝑠𝑀) = ((π‘ž Γ— π‘Ÿ) Β· 𝑀))
9074oveq2d 7425 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘žπ‘ (π‘Ÿπ‘ π‘€)) = (π‘žπ‘ (π‘Ÿ Β· 𝑀)))
9173oveqd 7426 . . . . . . . . . . . . . 14 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘žπ‘ (π‘Ÿ Β· 𝑀)) = (π‘ž Β· (π‘Ÿ Β· 𝑀)))
9290, 91eqtrd 2773 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (π‘žπ‘ (π‘Ÿπ‘ π‘€)) = (π‘ž Β· (π‘Ÿ Β· 𝑀)))
9389, 92eqeq12d 2749 . . . . . . . . . . . 12 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ↔ ((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀))))
9473oveqd 7426 . . . . . . . . . . . . 13 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ( 1 𝑠𝑀) = ( 1 Β· 𝑀))
9594eqeq1d 2735 . . . . . . . . . . . 12 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (( 1 𝑠𝑀) = 𝑀 ↔ ( 1 Β· 𝑀) = 𝑀))
9693, 95anbi12d 632 . . . . . . . . . . 11 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀) ↔ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))
9788, 96anbi12d 632 . . . . . . . . . 10 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)) ↔ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
98972ralbidv 3219 . . . . . . . . 9 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
9972, 98raleqbidv 3343 . . . . . . . 8 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)) ↔ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
10072, 99raleqbidv 3343 . . . . . . 7 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ (βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀)) ↔ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
101100anbi2d 630 . . . . . 6 ((𝑠 = Β· ∧ π‘˜ = 𝐾 ∧ 𝑝 = ⨣ ) β†’ ((𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))))
10269, 70, 71, 101sbc3ie 3864 . . . . 5 ([ Β· / 𝑠][𝐾 / π‘˜][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿπ‘ π‘€) ∈ 𝑉 ∧ (π‘Ÿπ‘ (𝑀 + π‘₯)) = ((π‘Ÿπ‘ π‘€) + (π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€) + (π‘Ÿπ‘ π‘€))) ∧ (((π‘ž Γ— π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ( 1 𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
10368, 102bitri 275 . . . 4 ([𝑉 / 𝑣][ + / π‘Ž][𝐹 / 𝑓][ Β· / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
10416, 103bitrdi 287 . . 3 (𝑔 = π‘Š β†’ ([(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀))) ↔ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))))
105 df-lmod 20473 . . 3 LMod = {𝑔 ∈ Grp ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][(Scalarβ€˜π‘”) / 𝑓][( ·𝑠 β€˜π‘”) / 𝑠][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ Ring ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀)))}
106104, 105elrab2 3687 . 2 (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))))
107 3anass 1096 . 2 ((π‘Š ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))) ↔ (π‘Š ∈ Grp ∧ (𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀)))))
108106, 107bitr4i 278 1 (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀))))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  [wsbc 3778  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  Grpcgrp 18819  1rcur 20004  Ringcrg 20056  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-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-lmod 20473
This theorem is referenced by:  lmodlema  20476  islmodd  20477  lmodgrp  20478  lmodring  20479  lmodprop2d  20534  isclmp  24613  lmodslmd  32349  ccfldsrarelvec  32745  lmod1  47173
  Copyright terms: Public domain W3C validator