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

Theorem isslmd 29086
 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 6113 . . . . 5 (Base‘𝑔) ∈ V
2 fvex 6113 . . . . 5 (+g𝑔) ∈ V
3 fvex 6113 . . . . . . 7 ( ·𝑠𝑔) ∈ V
4 fvex 6113 . . . . . . 7 (Scalar‘𝑔) ∈ V
5 fvex 6113 . . . . . . . . 9 (Base‘𝑓) ∈ V
6 fvex 6113 . . . . . . . . 9 (+g𝑓) ∈ V
7 fvex 6113 . . . . . . . . 9 (.r𝑓) ∈ V
8 simp1 1054 . . . . . . . . . . 11 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑘 = (Base‘𝑓))
9 simp2 1055 . . . . . . . . . . . . . . . . . 18 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑝 = (+g𝑓))
109oveqd 6566 . . . . . . . . . . . . . . . . 17 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (𝑞𝑝𝑟) = (𝑞(+g𝑓)𝑟))
1110oveq1d 6564 . . . . . . . . . . . . . . . 16 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞(+g𝑓)𝑟)𝑠𝑤))
1211eqeq1d 2612 . . . . . . . . . . . . . . 15 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))))
13123anbi3d 1397 . . . . . . . . . . . . . 14 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))))
14 simp3 1056 . . . . . . . . . . . . . . . . . 18 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑡 = (.r𝑓))
1514oveqd 6566 . . . . . . . . . . . . . . . . 17 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (𝑞𝑡𝑟) = (𝑞(.r𝑓)𝑟))
1615oveq1d 6564 . . . . . . . . . . . . . . . 16 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞(.r𝑓)𝑟)𝑠𝑤))
1716eqeq1d 2612 . . . . . . . . . . . . . . 15 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
18173anbi1d 1395 . . . . . . . . . . . . . 14 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)) ↔ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
1913, 18anbi12d 743 . . . . . . . . . . . . 13 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
20192ralbidv 2972 . . . . . . . . . . . 12 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
218, 20raleqbidv 3129 . . . . . . . . . . 11 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
228, 21raleqbidv 3129 . . . . . . . . . 10 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
2322anbi2d 736 . . . . . . . . 9 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝑓 ∈ SRing ∧ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))))
245, 6, 7, 23sbc3ie 3474 . . . . . . . 8 ([(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝑓 ∈ SRing ∧ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
25 simpr 476 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑓 = (Scalar‘𝑔))
2625eleq1d 2672 . . . . . . . . 9 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑓 ∈ SRing ↔ (Scalar‘𝑔) ∈ SRing))
2725fveq2d 6107 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (Base‘𝑓) = (Base‘(Scalar‘𝑔)))
28 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑠 = ( ·𝑠𝑔))
2928oveqd 6566 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑤) = (𝑟( ·𝑠𝑔)𝑤))
3029eleq1d 2672 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣))
3128oveqd 6566 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)))
3228oveqd 6566 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑥) = (𝑟( ·𝑠𝑔)𝑥))
3329, 32oveq12d 6567 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)))
3431, 33eqeq12d 2625 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥))))
3525fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (+g𝑓) = (+g‘(Scalar‘𝑔)))
3635oveqd 6566 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(+g𝑓)𝑟) = (𝑞(+g‘(Scalar‘𝑔))𝑟))
37 eqidd 2611 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑤 = 𝑤)
3828, 36, 37oveq123d 6570 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤))
3928oveqd 6566 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠𝑤) = (𝑞( ·𝑠𝑔)𝑤))
4039, 29oveq12d 6567 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)))
4138, 40eqeq12d 2625 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))))
4230, 34, 413anbi123d 1391 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)))))
4325fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (.r𝑓) = (.r‘(Scalar‘𝑔)))
4443oveqd 6566 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(.r𝑓)𝑟) = (𝑞(.r‘(Scalar‘𝑔))𝑟))
4528, 44, 37oveq123d 6570 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(.r𝑓)𝑟)𝑠𝑤) = ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤))
46 eqidd 2611 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑞 = 𝑞)
4728, 46, 29oveq123d 6570 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)))
4845, 47eqeq12d 2625 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤))))
4925fveq2d 6107 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (1r𝑓) = (1r‘(Scalar‘𝑔)))
5028, 49, 37oveq123d 6570 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((1r𝑓)𝑠𝑤) = ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤))
5150eqeq1d 2612 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((1r𝑓)𝑠𝑤) = 𝑤 ↔ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤))
5225fveq2d 6107 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (0g𝑓) = (0g‘(Scalar‘𝑔)))
5328, 52, 37oveq123d 6570 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((0g𝑓)𝑠𝑤) = ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤))
5453eqeq1d 2612 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((0g𝑓)𝑠𝑤) = (0g𝑔) ↔ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))
5548, 51, 543anbi123d 1391 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)) ↔ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))))
5642, 55anbi12d 743 . . . . . . . . . . . 12 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
57562ralbidv 2972 . . . . . . . . . . 11 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
5827, 57raleqbidv 3129 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
5927, 58raleqbidv 3129 . . . . . . . . 9 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑞 ∈ (Base‘(Scalar‘𝑔))∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
6026, 59anbi12d 743 . . . . . . . 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, 60syl5bb 271 . . . . . . 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 3472 . . . . . 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 472 . . . . . . . . 9 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → 𝑣 = (Base‘𝑔))
6463eleq2d 2673 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ↔ (𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔)))
65 simpr 476 . . . . . . . . . . . . . . 15 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → 𝑎 = (+g𝑔))
6665oveqd 6566 . . . . . . . . . . . . . 14 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (𝑤𝑎𝑥) = (𝑤(+g𝑔)𝑥))
6766oveq2d 6565 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)))
6865oveqd 6566 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)))
6967, 68eqeq12d 2625 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ↔ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥))))
7065oveqd 6566 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)))
7170eqeq2d 2620 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))))
7264, 69, 713anbi123d 1391 . . . . . . . . . . 11 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ↔ ((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)))))
7372anbi1d 737 . . . . . . . . . 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 3129 . . . . . . . . 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 3129 . . . . . . . 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 2972 . . . . . . 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 736 . . . . . 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, 77syl5bb 271 . . . . 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 3472 . . . 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 6103 . . . . . . 7 (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
81 isslmd.f . . . . . . 7 𝐹 = (Scalar‘𝑊)
8280, 81syl6eqr 2662 . . . . . 6 (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
8382eleq1d 2672 . . . . 5 (𝑔 = 𝑊 → ((Scalar‘𝑔) ∈ SRing ↔ 𝐹 ∈ SRing))
8482fveq2d 6107 . . . . . . 7 (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = (Base‘𝐹))
85 isslmd.k . . . . . . 7 𝐾 = (Base‘𝐹)
8684, 85syl6eqr 2662 . . . . . 6 (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = 𝐾)
87 fveq2 6103 . . . . . . . . 9 (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
88 isslmd.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
8987, 88syl6eqr 2662 . . . . . . . 8 (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
90 fveq2 6103 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → ( ·𝑠𝑔) = ( ·𝑠𝑊))
91 isslmd.s . . . . . . . . . . . . . 14 · = ( ·𝑠𝑊)
9290, 91syl6eqr 2662 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → ( ·𝑠𝑔) = · )
9392oveqd 6566 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)𝑤) = (𝑟 · 𝑤))
9493, 89eleq12d 2682 . . . . . . . . . . 11 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ↔ (𝑟 · 𝑤) ∈ 𝑉))
95 eqidd 2611 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑟 = 𝑟)
96 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (+g𝑔) = (+g𝑊))
97 isslmd.a . . . . . . . . . . . . . . 15 + = (+g𝑊)
9896, 97syl6eqr 2662 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (+g𝑔) = + )
9998oveqd 6566 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑤(+g𝑔)𝑥) = (𝑤 + 𝑥))
10092, 95, 99oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = (𝑟 · (𝑤 + 𝑥)))
10192oveqd 6566 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)𝑥) = (𝑟 · 𝑥))
10298, 93, 101oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
103100, 102eqeq12d 2625 . . . . . . . . . . 11 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
10482fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (+g‘(Scalar‘𝑔)) = (+g𝐹))
105 isslmd.p . . . . . . . . . . . . . . 15 = (+g𝐹)
106104, 105syl6eqr 2662 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (+g‘(Scalar‘𝑔)) = )
107106oveqd 6566 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞(+g‘(Scalar‘𝑔))𝑟) = (𝑞 𝑟))
108 eqidd 2611 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑤 = 𝑤)
10992, 107, 108oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞 𝑟) · 𝑤))
11092oveqd 6566 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞( ·𝑠𝑔)𝑤) = (𝑞 · 𝑤))
11198, 110, 93oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
112109, 111eqeq12d 2625 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
11394, 103, 1123anbi123d 1391 . . . . . . . . . 10 (𝑔 = 𝑊 → (((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
11482fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (.r‘(Scalar‘𝑔)) = (.r𝐹))
115 isslmd.t . . . . . . . . . . . . . . 15 × = (.r𝐹)
116114, 115syl6eqr 2662 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (.r‘(Scalar‘𝑔)) = × )
117116oveqd 6566 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞(.r‘(Scalar‘𝑔))𝑟) = (𝑞 × 𝑟))
11892, 117, 108oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞 × 𝑟) · 𝑤))
119 eqidd 2611 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑞 = 𝑞)
12092, 119, 93oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) = (𝑞 · (𝑟 · 𝑤)))
121118, 120eqeq12d 2625 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
12282fveq2d 6107 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (1r‘(Scalar‘𝑔)) = (1r𝐹))
123 isslmd.u . . . . . . . . . . . . . 14 1 = (1r𝐹)
124122, 123syl6eqr 2662 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (1r‘(Scalar‘𝑔)) = 1 )
12592, 124, 108oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = ( 1 · 𝑤))
126125eqeq1d 2612 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
12782fveq2d 6107 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (0g‘(Scalar‘𝑔)) = (0g𝐹))
128 isslmd.o . . . . . . . . . . . . . 14 𝑂 = (0g𝐹)
129127, 128syl6eqr 2662 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (0g‘(Scalar‘𝑔)) = 𝑂)
13092, 129, 108oveq123d 6570 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (𝑂 · 𝑤))
131 fveq2 6103 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (0g𝑔) = (0g𝑊))
132 isslmd.0 . . . . . . . . . . . . 13 0 = (0g𝑊)
133131, 132syl6eqr 2662 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (0g𝑔) = 0 )
134130, 133eqeq12d 2625 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔) ↔ (𝑂 · 𝑤) = 0 ))
135121, 126, 1343anbi123d 1391 . . . . . . . . . 10 (𝑔 = 𝑊 → ((((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
136113, 135anbi12d 743 . . . . . . . . 9 (𝑔 = 𝑊 → ((((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13789, 136raleqbidv 3129 . . . . . . . 8 (𝑔 = 𝑊 → (∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13889, 137raleqbidv 3129 . . . . . . 7 (𝑔 = 𝑊 → (∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13986, 138raleqbidv 3129 . . . . . 6 (𝑔 = 𝑊 → (∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
14086, 139raleqbidv 3129 . . . . 5 (𝑔 = 𝑊 → (∀𝑞 ∈ (Base‘(Scalar‘𝑔))∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
14183, 140anbi12d 743 . . . 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, 141syl5bb 271 . . 3 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
143 df-slmd 29085 . . 3 SLMod = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))}
144142, 143elrab2 3333 . 2 (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
145 3anass 1035 . 2 ((𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))) ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
146144, 145bitr4i 266 1 (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  [wsbc 3402  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +gcplusg 15768  .rcmulr 15769  Scalarcsca 15771   ·𝑠 cvsca 15772  0gc0g 15923  CMndccmn 18016  1rcur 18324  SRingcsrg 18328  SLModcslmd 29084 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-slmd 29085 This theorem is referenced by:  slmdlema  29087  lmodslmd  29088  slmdcmn  29089  slmdsrg  29091  xrge0slmod  29175
 Copyright terms: Public domain W3C validator