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

Theorem isslmd 30887
 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 6658 . . . . 5 (Base‘𝑔) ∈ V
2 fvex 6658 . . . . 5 (+g𝑔) ∈ V
3 fvex 6658 . . . . . . 7 ( ·𝑠𝑔) ∈ V
4 fvex 6658 . . . . . . 7 (Scalar‘𝑔) ∈ V
5 fvex 6658 . . . . . . . . 9 (Base‘𝑓) ∈ V
6 fvex 6658 . . . . . . . . 9 (+g𝑓) ∈ V
7 fvex 6658 . . . . . . . . 9 (.r𝑓) ∈ V
8 simp1 1133 . . . . . . . . . . 11 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑘 = (Base‘𝑓))
9 simp2 1134 . . . . . . . . . . . . . . . . . 18 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑝 = (+g𝑓))
109oveqd 7152 . . . . . . . . . . . . . . . . 17 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (𝑞𝑝𝑟) = (𝑞(+g𝑓)𝑟))
1110oveq1d 7150 . . . . . . . . . . . . . . . 16 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞(+g𝑓)𝑟)𝑠𝑤))
1211eqeq1d 2800 . . . . . . . . . . . . . . 15 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))))
13123anbi3d 1439 . . . . . . . . . . . . . 14 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))))
14 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → 𝑡 = (.r𝑓))
1514oveqd 7152 . . . . . . . . . . . . . . . . 17 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (𝑞𝑡𝑟) = (𝑞(.r𝑓)𝑟))
1615oveq1d 7150 . . . . . . . . . . . . . . . 16 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞(.r𝑓)𝑟)𝑠𝑤))
1716eqeq1d 2800 . . . . . . . . . . . . . . 15 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
18173anbi1d 1437 . . . . . . . . . . . . . 14 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)) ↔ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
1913, 18anbi12d 633 . . . . . . . . . . . . 13 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
20192ralbidv 3164 . . . . . . . . . . . 12 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
218, 20raleqbidv 3354 . . . . . . . . . . 11 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
228, 21raleqbidv 3354 . . . . . . . . . 10 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
2322anbi2d 631 . . . . . . . . 9 ((𝑘 = (Base‘𝑓) ∧ 𝑝 = (+g𝑓) ∧ 𝑡 = (.r𝑓)) → ((𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝑓 ∈ SRing ∧ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))))
245, 6, 7, 23sbc3ie 3798 . . . . . . . 8 ([(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝑓 ∈ SRing ∧ ∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))))
25 simpr 488 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑓 = (Scalar‘𝑔))
2625eleq1d 2874 . . . . . . . . 9 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑓 ∈ SRing ↔ (Scalar‘𝑔) ∈ SRing))
2725fveq2d 6649 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (Base‘𝑓) = (Base‘(Scalar‘𝑔)))
28 simpl 486 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑠 = ( ·𝑠𝑔))
2928oveqd 7152 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑤) = (𝑟( ·𝑠𝑔)𝑤))
3029eleq1d 2874 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣))
3128oveqd 7152 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)))
3228oveqd 7152 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑟𝑠𝑥) = (𝑟( ·𝑠𝑔)𝑥))
3329, 32oveq12d 7153 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)))
3431, 33eqeq12d 2814 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥))))
3525fveq2d 6649 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (+g𝑓) = (+g‘(Scalar‘𝑔)))
3635oveqd 7152 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(+g𝑓)𝑟) = (𝑞(+g‘(Scalar‘𝑔))𝑟))
37 eqidd 2799 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑤 = 𝑤)
3828, 36, 37oveq123d 7156 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤))
3928oveqd 7152 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠𝑤) = (𝑞( ·𝑠𝑔)𝑤))
4039, 29oveq12d 7153 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)))
4138, 40eqeq12d 2814 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))))
4230, 34, 413anbi123d 1433 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)))))
4325fveq2d 6649 . . . . . . . . . . . . . . . . 17 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (.r𝑓) = (.r‘(Scalar‘𝑔)))
4443oveqd 7152 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞(.r𝑓)𝑟) = (𝑞(.r‘(Scalar‘𝑔))𝑟))
4528, 44, 37oveq123d 7156 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((𝑞(.r𝑓)𝑟)𝑠𝑤) = ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤))
46 eqidd 2799 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → 𝑞 = 𝑞)
4728, 46, 29oveq123d 7156 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)))
4845, 47eqeq12d 2814 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤))))
4925fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (1r𝑓) = (1r‘(Scalar‘𝑔)))
5028, 49, 37oveq123d 7156 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((1r𝑓)𝑠𝑤) = ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤))
5150eqeq1d 2800 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((1r𝑓)𝑠𝑤) = 𝑤 ↔ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤))
5225fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (0g𝑓) = (0g‘(Scalar‘𝑔)))
5328, 52, 37oveq123d 7156 . . . . . . . . . . . . . . 15 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((0g𝑓)𝑠𝑤) = ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤))
5453eqeq1d 2800 . . . . . . . . . . . . . 14 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (((0g𝑓)𝑠𝑤) = (0g𝑔) ↔ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))
5548, 51, 543anbi123d 1433 . . . . . . . . . . . . 13 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)) ↔ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))))
5642, 55anbi12d 633 . . . . . . . . . . . 12 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
57562ralbidv 3164 . . . . . . . . . . 11 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
5827, 57raleqbidv 3354 . . . . . . . . . 10 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
5927, 58raleqbidv 3354 . . . . . . . . 9 ((𝑠 = ( ·𝑠𝑔) ∧ 𝑓 = (Scalar‘𝑔)) → (∀𝑞 ∈ (Base‘𝑓)∀𝑟 ∈ (Base‘𝑓)∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞(+g𝑓)𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞(.r𝑓)𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))) ↔ ∀𝑞 ∈ (Base‘(Scalar‘𝑔))∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥𝑣𝑤𝑣 (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)))))
6026, 59anbi12d 633 . . . . . . . 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 286 . . . . . . 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 3796 . . . . . 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 486 . . . . . . . . 9 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → 𝑣 = (Base‘𝑔))
6463eleq2d 2875 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ↔ (𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔)))
65 simpr 488 . . . . . . . . . . . . . . 15 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → 𝑎 = (+g𝑔))
6665oveqd 7152 . . . . . . . . . . . . . 14 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (𝑤𝑎𝑥) = (𝑤(+g𝑔)𝑥))
6766oveq2d 7151 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)))
6865oveqd 7152 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)))
6967, 68eqeq12d 2814 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ↔ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥))))
7065oveqd 7152 . . . . . . . . . . . . 13 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)))
7170eqeq2d 2809 . . . . . . . . . . . 12 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))))
7264, 69, 713anbi123d 1433 . . . . . . . . . . 11 ((𝑣 = (Base‘𝑔) ∧ 𝑎 = (+g𝑔)) → (((𝑟( ·𝑠𝑔)𝑤) ∈ 𝑣 ∧ (𝑟( ·𝑠𝑔)(𝑤𝑎𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)𝑎(𝑟( ·𝑠𝑔)𝑤))) ↔ ((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)))))
7372anbi1d 632 . . . . . . . . . 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 3354 . . . . . . . . 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 3354 . . . . . . . 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 3164 . . . . . . 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 631 . . . . . 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 286 . . . . 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 3796 . . . 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 6645 . . . . . . 7 (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
81 isslmd.f . . . . . . 7 𝐹 = (Scalar‘𝑊)
8280, 81eqtr4di 2851 . . . . . 6 (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
8382eleq1d 2874 . . . . 5 (𝑔 = 𝑊 → ((Scalar‘𝑔) ∈ SRing ↔ 𝐹 ∈ SRing))
8482fveq2d 6649 . . . . . . 7 (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = (Base‘𝐹))
85 isslmd.k . . . . . . 7 𝐾 = (Base‘𝐹)
8684, 85eqtr4di 2851 . . . . . 6 (𝑔 = 𝑊 → (Base‘(Scalar‘𝑔)) = 𝐾)
87 fveq2 6645 . . . . . . . . 9 (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
88 isslmd.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
8987, 88eqtr4di 2851 . . . . . . . 8 (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
90 fveq2 6645 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → ( ·𝑠𝑔) = ( ·𝑠𝑊))
91 isslmd.s . . . . . . . . . . . . . 14 · = ( ·𝑠𝑊)
9290, 91eqtr4di 2851 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → ( ·𝑠𝑔) = · )
9392oveqd 7152 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)𝑤) = (𝑟 · 𝑤))
9493, 89eleq12d 2884 . . . . . . . . . . 11 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ↔ (𝑟 · 𝑤) ∈ 𝑉))
95 eqidd 2799 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑟 = 𝑟)
96 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (+g𝑔) = (+g𝑊))
97 isslmd.a . . . . . . . . . . . . . . 15 + = (+g𝑊)
9896, 97eqtr4di 2851 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (+g𝑔) = + )
9998oveqd 7152 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑤(+g𝑔)𝑥) = (𝑤 + 𝑥))
10092, 95, 99oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = (𝑟 · (𝑤 + 𝑥)))
10192oveqd 7152 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑟( ·𝑠𝑔)𝑥) = (𝑟 · 𝑥))
10298, 93, 101oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
103100, 102eqeq12d 2814 . . . . . . . . . . 11 (𝑔 = 𝑊 → ((𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
10482fveq2d 6649 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (+g‘(Scalar‘𝑔)) = (+g𝐹))
105 isslmd.p . . . . . . . . . . . . . . 15 = (+g𝐹)
106104, 105eqtr4di 2851 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (+g‘(Scalar‘𝑔)) = )
107106oveqd 7152 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞(+g‘(Scalar‘𝑔))𝑟) = (𝑞 𝑟))
108 eqidd 2799 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑤 = 𝑤)
10992, 107, 108oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞 𝑟) · 𝑤))
11092oveqd 7152 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞( ·𝑠𝑔)𝑤) = (𝑞 · 𝑤))
11198, 110, 93oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
112109, 111eqeq12d 2814 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
11394, 103, 1123anbi123d 1433 . . . . . . . . . 10 (𝑔 = 𝑊 → (((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
11482fveq2d 6649 . . . . . . . . . . . . . . 15 (𝑔 = 𝑊 → (.r‘(Scalar‘𝑔)) = (.r𝐹))
115 isslmd.t . . . . . . . . . . . . . . 15 × = (.r𝐹)
116114, 115eqtr4di 2851 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (.r‘(Scalar‘𝑔)) = × )
117116oveqd 7152 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (𝑞(.r‘(Scalar‘𝑔))𝑟) = (𝑞 × 𝑟))
11892, 117, 108oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞 × 𝑟) · 𝑤))
119 eqidd 2799 . . . . . . . . . . . . 13 (𝑔 = 𝑊𝑞 = 𝑞)
12092, 119, 93oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) = (𝑞 · (𝑟 · 𝑤)))
121118, 120eqeq12d 2814 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
12282fveq2d 6649 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (1r‘(Scalar‘𝑔)) = (1r𝐹))
123 isslmd.u . . . . . . . . . . . . . 14 1 = (1r𝐹)
124122, 123eqtr4di 2851 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (1r‘(Scalar‘𝑔)) = 1 )
12592, 124, 108oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = ( 1 · 𝑤))
126125eqeq1d 2800 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
12782fveq2d 6649 . . . . . . . . . . . . . 14 (𝑔 = 𝑊 → (0g‘(Scalar‘𝑔)) = (0g𝐹))
128 isslmd.o . . . . . . . . . . . . . 14 𝑂 = (0g𝐹)
129127, 128eqtr4di 2851 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (0g‘(Scalar‘𝑔)) = 𝑂)
13092, 129, 108oveq123d 7156 . . . . . . . . . . . 12 (𝑔 = 𝑊 → ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (𝑂 · 𝑤))
131 fveq2 6645 . . . . . . . . . . . . 13 (𝑔 = 𝑊 → (0g𝑔) = (0g𝑊))
132 isslmd.0 . . . . . . . . . . . . 13 0 = (0g𝑊)
133131, 132eqtr4di 2851 . . . . . . . . . . . 12 (𝑔 = 𝑊 → (0g𝑔) = 0 )
134130, 133eqeq12d 2814 . . . . . . . . . . 11 (𝑔 = 𝑊 → (((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔) ↔ (𝑂 · 𝑤) = 0 ))
135121, 126, 1343anbi123d 1433 . . . . . . . . . 10 (𝑔 = 𝑊 → ((((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔)) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))
136113, 135anbi12d 633 . . . . . . . . 9 (𝑔 = 𝑊 → ((((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13789, 136raleqbidv 3354 . . . . . . . 8 (𝑔 = 𝑊 → (∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13889, 137raleqbidv 3354 . . . . . . 7 (𝑔 = 𝑊 → (∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
13986, 138raleqbidv 3354 . . . . . 6 (𝑔 = 𝑊 → (∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
14086, 139raleqbidv 3354 . . . . 5 (𝑔 = 𝑊 → (∀𝑞 ∈ (Base‘(Scalar‘𝑔))∀𝑟 ∈ (Base‘(Scalar‘𝑔))∀𝑥 ∈ (Base‘𝑔)∀𝑤 ∈ (Base‘𝑔)(((𝑟( ·𝑠𝑔)𝑤) ∈ (Base‘𝑔) ∧ (𝑟( ·𝑠𝑔)(𝑤(+g𝑔)𝑥)) = ((𝑟( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = ((𝑞( ·𝑠𝑔)𝑤)(+g𝑔)(𝑟( ·𝑠𝑔)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑔))𝑟)( ·𝑠𝑔)𝑤) = (𝑞( ·𝑠𝑔)(𝑟( ·𝑠𝑔)𝑤)) ∧ ((1r‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = 𝑤 ∧ ((0g‘(Scalar‘𝑔))( ·𝑠𝑔)𝑤) = (0g𝑔))) ↔ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
14183, 140anbi12d 633 . . . 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 286 . . 3 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))) ↔ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
143 df-slmd 30886 . . 3 SLMod = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))}
144142, 143elrab2 3631 . 2 (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
145 3anass 1092 . 2 ((𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))) ↔ (𝑊 ∈ CMnd ∧ (𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 )))))
146144, 145bitr4i 281 1 (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ 𝐹 ∈ SRing ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤 ∧ (𝑂 · 𝑤) = 0 ))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  [wsbc 3720  ‘cfv 6324  (class class class)co 7135  Basecbs 16477  +gcplusg 16559  .rcmulr 16560  Scalarcsca 16562   ·𝑠 cvsca 16563  0gc0g 16707  CMndccmn 18901  1rcur 19247  SRingcsrg 19251  SLModcslmd 30885 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-slmd 30886 This theorem is referenced by:  slmdlema  30888  lmodslmd  30889  slmdcmn  30890  slmdsrg  30892  xrge0slmod  30975
 Copyright terms: Public domain W3C validator