Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isslmd Structured version   Visualization version   GIF version

Theorem isslmd 32851
Description: The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
Hypotheses
Ref Expression
isslmd.v 𝑉 = (Baseβ€˜π‘Š)
isslmd.a + = (+gβ€˜π‘Š)
isslmd.s Β· = ( ·𝑠 β€˜π‘Š)
isslmd.0 0 = (0gβ€˜π‘Š)
isslmd.f 𝐹 = (Scalarβ€˜π‘Š)
isslmd.k 𝐾 = (Baseβ€˜πΉ)
isslmd.p ⨣ = (+gβ€˜πΉ)
isslmd.t Γ— = (.rβ€˜πΉ)
isslmd.u 1 = (1rβ€˜πΉ)
isslmd.o 𝑂 = (0gβ€˜πΉ)
Assertion
Ref Expression
isslmd (π‘Š ∈ SLMod ↔ (π‘Š ∈ CMnd ∧ 𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
Distinct variable groups:   π‘Ÿ,π‘ž,𝑀,π‘₯, Γ—   + ,π‘ž,π‘Ÿ,𝑀,π‘₯   ⨣ ,π‘ž,π‘Ÿ,𝑀,π‘₯   1 ,π‘ž,π‘Ÿ,𝑀,π‘₯   Β· ,π‘ž,π‘Ÿ,𝑀,π‘₯   𝐹,π‘ž,π‘Ÿ,𝑀,π‘₯   𝐾,π‘ž,π‘Ÿ,𝑀,π‘₯   𝑉,π‘ž,π‘Ÿ,𝑀,π‘₯   π‘Š,π‘ž,π‘Ÿ,𝑀,π‘₯   0 ,π‘ž,π‘Ÿ,𝑀,π‘₯   𝑂,π‘ž,π‘Ÿ,𝑀,π‘₯

Proof of Theorem isslmd
Dummy variables 𝑓 π‘Ž 𝑔 π‘˜ 𝑝 𝑠 𝑑 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6897 . . . . 5 (Baseβ€˜π‘”) ∈ V
2 fvex 6897 . . . . 5 (+gβ€˜π‘”) ∈ V
3 fvex 6897 . . . . . . 7 ( ·𝑠 β€˜π‘”) ∈ V
4 fvex 6897 . . . . . . 7 (Scalarβ€˜π‘”) ∈ V
5 fvex 6897 . . . . . . . . 9 (Baseβ€˜π‘“) ∈ V
6 fvex 6897 . . . . . . . . 9 (+gβ€˜π‘“) ∈ V
7 fvex 6897 . . . . . . . . 9 (.rβ€˜π‘“) ∈ V
8 simp1 1133 . . . . . . . . . . 11 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ π‘˜ = (Baseβ€˜π‘“))
9 simp2 1134 . . . . . . . . . . . . . . . . . 18 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ 𝑝 = (+gβ€˜π‘“))
109oveqd 7421 . . . . . . . . . . . . . . . . 17 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (π‘žπ‘π‘Ÿ) = (π‘ž(+gβ€˜π‘“)π‘Ÿ))
1110oveq1d 7419 . . . . . . . . . . . . . . . 16 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀))
1211eqeq1d 2728 . . . . . . . . . . . . . . 15 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)) ↔ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))))
13123anbi3d 1438 . . . . . . . . . . . . . 14 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ↔ ((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)))))
14 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ 𝑑 = (.rβ€˜π‘“))
1514oveqd 7421 . . . . . . . . . . . . . . . . 17 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (π‘žπ‘‘π‘Ÿ) = (π‘ž(.rβ€˜π‘“)π‘Ÿ))
1615oveq1d 7419 . . . . . . . . . . . . . . . 16 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ ((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = ((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀))
1716eqeq1d 2728 . . . . . . . . . . . . . . 15 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ↔ ((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€))))
18173anbi1d 1436 . . . . . . . . . . . . . 14 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ ((((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)) ↔ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
1913, 18anbi12d 630 . . . . . . . . . . . . 13 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ ((((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))))
20192ralbidv 3212 . . . . . . . . . . . 12 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))))
218, 20raleqbidv 3336 . . . . . . . . . . 11 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))))
228, 21raleqbidv 3336 . . . . . . . . . 10 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ (βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘ž ∈ (Baseβ€˜π‘“)βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))))
2322anbi2d 628 . . . . . . . . 9 ((π‘˜ = (Baseβ€˜π‘“) ∧ 𝑝 = (+gβ€˜π‘“) ∧ 𝑑 = (.rβ€˜π‘“)) β†’ ((𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ (𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜π‘“)βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))))
245, 6, 7, 23sbc3ie 3858 . . . . . . . 8 ([(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ (𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜π‘“)βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))))
25 simpr 484 . . . . . . . . . 10 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ 𝑓 = (Scalarβ€˜π‘”))
2625eleq1d 2812 . . . . . . . . 9 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (𝑓 ∈ SRing ↔ (Scalarβ€˜π‘”) ∈ SRing))
2725fveq2d 6888 . . . . . . . . . 10 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (Baseβ€˜π‘“) = (Baseβ€˜(Scalarβ€˜π‘”)))
28 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ 𝑠 = ( ·𝑠 β€˜π‘”))
2928oveqd 7421 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘Ÿπ‘ π‘€) = (π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))
3029eleq1d 2812 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘Ÿπ‘ π‘€) ∈ 𝑣 ↔ (π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣))
3128oveqd 7421 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)))
3228oveqd 7421 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘Ÿπ‘ π‘₯) = (π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯))
3329, 32oveq12d 7422 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)))
3431, 33eqeq12d 2742 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ↔ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯))))
3525fveq2d 6888 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (+gβ€˜π‘“) = (+gβ€˜(Scalarβ€˜π‘”)))
3635oveqd 7421 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘ž(+gβ€˜π‘“)π‘Ÿ) = (π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ))
37 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ 𝑀 = 𝑀)
3828, 36, 37oveq123d 7425 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀))
3928oveqd 7421 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘žπ‘ π‘€) = (π‘ž( ·𝑠 β€˜π‘”)𝑀))
4039, 29oveq12d 7422 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)))
4138, 40eqeq12d 2742 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)) ↔ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))))
4230, 34, 413anbi123d 1432 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ↔ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)))))
4325fveq2d 6888 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (.rβ€˜π‘“) = (.rβ€˜(Scalarβ€˜π‘”)))
4443oveqd 7421 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘ž(.rβ€˜π‘“)π‘Ÿ) = (π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ))
4528, 44, 37oveq123d 7425 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀))
46 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ π‘ž = π‘ž)
4728, 46, 29oveq123d 7425 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (π‘žπ‘ (π‘Ÿπ‘ π‘€)) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)))
4845, 47eqeq12d 2742 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ↔ ((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))))
4925fveq2d 6888 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (1rβ€˜π‘“) = (1rβ€˜(Scalarβ€˜π‘”)))
5028, 49, 37oveq123d 7425 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((1rβ€˜π‘“)𝑠𝑀) = ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀))
5150eqeq1d 2728 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ↔ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀))
5225fveq2d 6888 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (0gβ€˜π‘“) = (0gβ€˜(Scalarβ€˜π‘”)))
5328, 52, 37oveq123d 7425 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((0gβ€˜π‘“)𝑠𝑀) = ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀))
5453eqeq1d 2728 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”) ↔ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))
5548, 51, 543anbi123d 1432 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)) ↔ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))))
5642, 55anbi12d 630 . . . . . . . . . . . 12 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
57562ralbidv 3212 . . . . . . . . . . 11 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
5827, 57raleqbidv 3336 . . . . . . . . . 10 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
5927, 58raleqbidv 3336 . . . . . . . . 9 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ (βˆ€π‘ž ∈ (Baseβ€˜π‘“)βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
6026, 59anbi12d 630 . . . . . . . 8 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ((𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜π‘“)βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘ž(+gβ€˜π‘“)π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘ž(.rβ€˜π‘“)π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))))))
6124, 60bitrid 283 . . . . . . 7 ((𝑠 = ( ·𝑠 β€˜π‘”) ∧ 𝑓 = (Scalarβ€˜π‘”)) β†’ ([(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))))))
623, 4, 61sbc2ie 3855 . . . . . 6 ([( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
63 simpl 482 . . . . . . . . 9 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ 𝑣 = (Baseβ€˜π‘”))
6463eleq2d 2813 . . . . . . . . . . . 12 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ↔ (π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”)))
65 simpr 484 . . . . . . . . . . . . . . 15 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ π‘Ž = (+gβ€˜π‘”))
6665oveqd 7421 . . . . . . . . . . . . . 14 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (π‘€π‘Žπ‘₯) = (𝑀(+gβ€˜π‘”)π‘₯))
6766oveq2d 7420 . . . . . . . . . . . . 13 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)))
6865oveqd 7421 . . . . . . . . . . . . 13 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)))
6967, 68eqeq12d 2742 . . . . . . . . . . . 12 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ↔ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯))))
7065oveqd 7421 . . . . . . . . . . . . 13 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)))
7170eqeq2d 2737 . . . . . . . . . . . 12 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ↔ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))))
7264, 69, 713anbi123d 1432 . . . . . . . . . . 11 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ↔ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)))))
7372anbi1d 629 . . . . . . . . . 10 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ((((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
7463, 73raleqbidv 3336 . . . . . . . . 9 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
7563, 74raleqbidv 3336 . . . . . . . 8 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
76752ralbidv 3212 . . . . . . 7 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
7776anbi2d 628 . . . . . 6 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ (((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ 𝑣 ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(π‘€π‘Žπ‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)π‘Ž(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))))))
7862, 77bitrid 283 . . . . 5 ((𝑣 = (Baseβ€˜π‘”) ∧ π‘Ž = (+gβ€˜π‘”)) β†’ ([( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))))))
791, 2, 78sbc2ie 3855 . . . 4 ([(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ ((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))))
80 fveq2 6884 . . . . . . 7 (𝑔 = π‘Š β†’ (Scalarβ€˜π‘”) = (Scalarβ€˜π‘Š))
81 isslmd.f . . . . . . 7 𝐹 = (Scalarβ€˜π‘Š)
8280, 81eqtr4di 2784 . . . . . 6 (𝑔 = π‘Š β†’ (Scalarβ€˜π‘”) = 𝐹)
8382eleq1d 2812 . . . . 5 (𝑔 = π‘Š β†’ ((Scalarβ€˜π‘”) ∈ SRing ↔ 𝐹 ∈ SRing))
8482fveq2d 6888 . . . . . . 7 (𝑔 = π‘Š β†’ (Baseβ€˜(Scalarβ€˜π‘”)) = (Baseβ€˜πΉ))
85 isslmd.k . . . . . . 7 𝐾 = (Baseβ€˜πΉ)
8684, 85eqtr4di 2784 . . . . . 6 (𝑔 = π‘Š β†’ (Baseβ€˜(Scalarβ€˜π‘”)) = 𝐾)
87 fveq2 6884 . . . . . . . . 9 (𝑔 = π‘Š β†’ (Baseβ€˜π‘”) = (Baseβ€˜π‘Š))
88 isslmd.v . . . . . . . . 9 𝑉 = (Baseβ€˜π‘Š)
8987, 88eqtr4di 2784 . . . . . . . 8 (𝑔 = π‘Š β†’ (Baseβ€˜π‘”) = 𝑉)
90 fveq2 6884 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ ( ·𝑠 β€˜π‘”) = ( ·𝑠 β€˜π‘Š))
91 isslmd.s . . . . . . . . . . . . . 14 Β· = ( ·𝑠 β€˜π‘Š)
9290, 91eqtr4di 2784 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ ( ·𝑠 β€˜π‘”) = Β· )
9392oveqd 7421 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ (π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) = (π‘Ÿ Β· 𝑀))
9493, 89eleq12d 2821 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ↔ (π‘Ÿ Β· 𝑀) ∈ 𝑉))
95 eqidd 2727 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ π‘Ÿ = π‘Ÿ)
96 fveq2 6884 . . . . . . . . . . . . . . 15 (𝑔 = π‘Š β†’ (+gβ€˜π‘”) = (+gβ€˜π‘Š))
97 isslmd.a . . . . . . . . . . . . . . 15 + = (+gβ€˜π‘Š)
9896, 97eqtr4di 2784 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ (+gβ€˜π‘”) = + )
9998oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (𝑀(+gβ€˜π‘”)π‘₯) = (𝑀 + π‘₯))
10092, 95, 99oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = (π‘Ÿ Β· (𝑀 + π‘₯)))
10192oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯) = (π‘Ÿ Β· π‘₯))
10298, 93, 101oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)))
103100, 102eqeq12d 2742 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ ((π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ↔ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯))))
10482fveq2d 6888 . . . . . . . . . . . . . . 15 (𝑔 = π‘Š β†’ (+gβ€˜(Scalarβ€˜π‘”)) = (+gβ€˜πΉ))
105 isslmd.p . . . . . . . . . . . . . . 15 ⨣ = (+gβ€˜πΉ)
106104, 105eqtr4di 2784 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ (+gβ€˜(Scalarβ€˜π‘”)) = ⨣ )
107106oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ) = (π‘ž ⨣ π‘Ÿ))
108 eqidd 2727 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ 𝑀 = 𝑀)
10992, 107, 108oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž ⨣ π‘Ÿ) Β· 𝑀))
11092oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (π‘ž( ·𝑠 β€˜π‘”)𝑀) = (π‘ž Β· 𝑀))
11198, 110, 93oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)))
112109, 111eqeq12d 2742 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ (((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ↔ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))))
11394, 103, 1123anbi123d 1432 . . . . . . . . . 10 (𝑔 = π‘Š β†’ (((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ↔ ((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀)))))
11482fveq2d 6888 . . . . . . . . . . . . . . 15 (𝑔 = π‘Š β†’ (.rβ€˜(Scalarβ€˜π‘”)) = (.rβ€˜πΉ))
115 isslmd.t . . . . . . . . . . . . . . 15 Γ— = (.rβ€˜πΉ)
116114, 115eqtr4di 2784 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ (.rβ€˜(Scalarβ€˜π‘”)) = Γ— )
117116oveqd 7421 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ) = (π‘ž Γ— π‘Ÿ))
11892, 117, 108oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž Γ— π‘Ÿ) Β· 𝑀))
119 eqidd 2727 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ π‘ž = π‘ž)
12092, 119, 93oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) = (π‘ž Β· (π‘Ÿ Β· 𝑀)))
121118, 120eqeq12d 2742 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ↔ ((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀))))
12282fveq2d 6888 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ (1rβ€˜(Scalarβ€˜π‘”)) = (1rβ€˜πΉ))
123 isslmd.u . . . . . . . . . . . . . 14 1 = (1rβ€˜πΉ)
124122, 123eqtr4di 2784 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (1rβ€˜(Scalarβ€˜π‘”)) = 1 )
12592, 124, 108oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = ( 1 Β· 𝑀))
126125eqeq1d 2728 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ (((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ↔ ( 1 Β· 𝑀) = 𝑀))
12782fveq2d 6888 . . . . . . . . . . . . . 14 (𝑔 = π‘Š β†’ (0gβ€˜(Scalarβ€˜π‘”)) = (0gβ€˜πΉ))
128 isslmd.o . . . . . . . . . . . . . 14 𝑂 = (0gβ€˜πΉ)
129127, 128eqtr4di 2784 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (0gβ€˜(Scalarβ€˜π‘”)) = 𝑂)
13092, 129, 108oveq123d 7425 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (𝑂 Β· 𝑀))
131 fveq2 6884 . . . . . . . . . . . . 13 (𝑔 = π‘Š β†’ (0gβ€˜π‘”) = (0gβ€˜π‘Š))
132 isslmd.0 . . . . . . . . . . . . 13 0 = (0gβ€˜π‘Š)
133131, 132eqtr4di 2784 . . . . . . . . . . . 12 (𝑔 = π‘Š β†’ (0gβ€˜π‘”) = 0 )
134130, 133eqeq12d 2742 . . . . . . . . . . 11 (𝑔 = π‘Š β†’ (((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”) ↔ (𝑂 Β· 𝑀) = 0 ))
135121, 126, 1343anbi123d 1432 . . . . . . . . . 10 (𝑔 = π‘Š β†’ ((((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)) ↔ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))
136113, 135anbi12d 630 . . . . . . . . 9 (𝑔 = π‘Š β†’ ((((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
13789, 136raleqbidv 3336 . . . . . . . 8 (𝑔 = π‘Š β†’ (βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
13889, 137raleqbidv 3336 . . . . . . 7 (𝑔 = π‘Š β†’ (βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
13986, 138raleqbidv 3336 . . . . . 6 (𝑔 = π‘Š β†’ (βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
14086, 139raleqbidv 3336 . . . . 5 (𝑔 = π‘Š β†’ (βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”))) ↔ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
14183, 140anbi12d 630 . . . 4 (𝑔 = π‘Š β†’ (((Scalarβ€˜π‘”) ∈ SRing ∧ βˆ€π‘ž ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘Ÿ ∈ (Baseβ€˜(Scalarβ€˜π‘”))βˆ€π‘₯ ∈ (Baseβ€˜π‘”)βˆ€π‘€ ∈ (Baseβ€˜π‘”)(((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀) ∈ (Baseβ€˜π‘”) ∧ (π‘Ÿ( ·𝑠 β€˜π‘”)(𝑀(+gβ€˜π‘”)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)π‘₯)) ∧ ((π‘ž(+gβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = ((π‘ž( ·𝑠 β€˜π‘”)𝑀)(+gβ€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀))) ∧ (((π‘ž(.rβ€˜(Scalarβ€˜π‘”))π‘Ÿ)( ·𝑠 β€˜π‘”)𝑀) = (π‘ž( ·𝑠 β€˜π‘”)(π‘Ÿ( ·𝑠 β€˜π‘”)𝑀)) ∧ ((1rβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = 𝑀 ∧ ((0gβ€˜(Scalarβ€˜π‘”))( ·𝑠 β€˜π‘”)𝑀) = (0gβ€˜π‘”)))) ↔ (𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))))
14279, 141bitrid 283 . . 3 (𝑔 = π‘Š β†’ ([(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))) ↔ (𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))))
143 df-slmd 32850 . . 3 SLMod = {𝑔 ∈ CMnd ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))}
144142, 143elrab2 3681 . 2 (π‘Š ∈ SLMod ↔ (π‘Š ∈ CMnd ∧ (𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))))
145 3anass 1092 . 2 ((π‘Š ∈ CMnd ∧ 𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))) ↔ (π‘Š ∈ CMnd ∧ (𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 )))))
146144, 145bitr4i 278 1 (π‘Š ∈ SLMod ↔ (π‘Š ∈ CMnd ∧ 𝐹 ∈ SRing ∧ βˆ€π‘ž ∈ 𝐾 βˆ€π‘Ÿ ∈ 𝐾 βˆ€π‘₯ ∈ 𝑉 βˆ€π‘€ ∈ 𝑉 (((π‘Ÿ Β· 𝑀) ∈ 𝑉 ∧ (π‘Ÿ Β· (𝑀 + π‘₯)) = ((π‘Ÿ Β· 𝑀) + (π‘Ÿ Β· π‘₯)) ∧ ((π‘ž ⨣ π‘Ÿ) Β· 𝑀) = ((π‘ž Β· 𝑀) + (π‘Ÿ Β· 𝑀))) ∧ (((π‘ž Γ— π‘Ÿ) Β· 𝑀) = (π‘ž Β· (π‘Ÿ Β· 𝑀)) ∧ ( 1 Β· 𝑀) = 𝑀 ∧ (𝑂 Β· 𝑀) = 0 ))))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  [wsbc 3772  β€˜cfv 6536  (class class class)co 7404  Basecbs 17151  +gcplusg 17204  .rcmulr 17205  Scalarcsca 17207   ·𝑠 cvsca 17208  0gc0g 17392  CMndccmn 19698  1rcur 20084  SRingcsrg 20089  SLModcslmd 32849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-slmd 32850
This theorem is referenced by:  slmdlema  32852  lmodslmd  32853  slmdcmn  32854  slmdsrg  32856  xrge0slmod  32966
  Copyright terms: Public domain W3C validator