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

Theorem islmod 19637
Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
islmod.v 𝑉 = (Base‘𝑊)
islmod.a + = (+g𝑊)
islmod.s · = ( ·𝑠𝑊)
islmod.f 𝐹 = (Scalar‘𝑊)
islmod.k 𝐾 = (Base‘𝐹)
islmod.p = (+g𝐹)
islmod.t × = (.r𝐹)
islmod.u 1 = (1r𝐹)
Assertion
Ref Expression
islmod (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
Distinct variable groups:   𝑟,𝑞,𝑤,𝑥,𝐹   𝐾,𝑞,𝑟,𝑤,𝑥   ,𝑞,𝑟,𝑤,𝑥   𝑉,𝑞,𝑟,𝑤,𝑥   + ,𝑞,𝑟,𝑤,𝑥   1 ,𝑞,𝑟,𝑤,𝑥   × ,𝑞,𝑟,𝑤,𝑥   · ,𝑞,𝑟,𝑤,𝑥
Allowed substitution hints:   𝑊(𝑥,𝑤,𝑟,𝑞)

Proof of Theorem islmod
Dummy variables 𝑓 𝑎 𝑔 𝑘 𝑝 𝑠 𝑣 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6669 . . . . . 6 (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
2 islmod.v . . . . . 6 𝑉 = (Base‘𝑊)
31, 2syl6eqr 2874 . . . . 5 (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
4 fveq2 6669 . . . . . . 7 (𝑔 = 𝑊 → (+g𝑔) = (+g𝑊))
5 islmod.a . . . . . . 7 + = (+g𝑊)
64, 5syl6eqr 2874 . . . . . 6 (𝑔 = 𝑊 → (+g𝑔) = + )
7 fveq2 6669 . . . . . . . 8 (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
8 islmod.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
97, 8syl6eqr 2874 . . . . . . 7 (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
10 fveq2 6669 . . . . . . . . 9 (𝑔 = 𝑊 → ( ·𝑠𝑔) = ( ·𝑠𝑊))
11 islmod.s . . . . . . . . 9 · = ( ·𝑠𝑊)
1210, 11syl6eqr 2874 . . . . . . . 8 (𝑔 = 𝑊 → ( ·𝑠𝑔) = · )
1312sbceq1d 3776 . . . . . . 7 (𝑔 = 𝑊 → ([( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
149, 13sbceqbid 3778 . . . . . 6 (𝑔 = 𝑊 → ([(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
156, 14sbceqbid 3778 . . . . 5 (𝑔 = 𝑊 → ([(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
163, 15sbceqbid 3778 . . . 4 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
172fvexi 6683 . . . . . 6 𝑉 ∈ V
185fvexi 6683 . . . . . 6 + ∈ V
198fvexi 6683 . . . . . 6 𝐹 ∈ V
20 simp3 1134 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑓 = 𝐹)
2120fveq2d 6673 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
22 islmod.k . . . . . . . . 9 𝐾 = (Base‘𝐹)
2321, 22syl6eqr 2874 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
2420fveq2d 6673 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = (+g𝐹))
25 islmod.p . . . . . . . . . 10 = (+g𝐹)
2624, 25syl6eqr 2874 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = )
2720fveq2d 6673 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = (.r𝐹))
28 islmod.t . . . . . . . . . . . 12 × = (.r𝐹)
2927, 28syl6eqr 2874 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = × )
3029sbceq1d 3776 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
3128fvexi 6683 . . . . . . . . . . . 12 × ∈ V
32 oveq 7161 . . . . . . . . . . . . . . . . . . 19 (𝑡 = × → (𝑞𝑡𝑟) = (𝑞 × 𝑟))
3332oveq1d 7170 . . . . . . . . . . . . . . . . . 18 (𝑡 = × → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞 × 𝑟)𝑠𝑤))
3433eqeq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑡 = × → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
3534anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑡 = × → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
3635anbi2d 630 . . . . . . . . . . . . . . 15 (𝑡 = × → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
37362ralbidv 3199 . . . . . . . . . . . . . 14 (𝑡 = × → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
38372ralbidv 3199 . . . . . . . . . . . . 13 (𝑡 = × → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
3938anbi2d 630 . . . . . . . . . . . 12 (𝑡 = × → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
4031, 39sbcie 3811 . . . . . . . . . . 11 ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
4120eleq1d 2897 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑓 ∈ Ring ↔ 𝐹 ∈ Ring))
42 simp1 1132 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑣 = 𝑉)
4342eleq2d 2898 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟𝑠𝑤) ∈ 𝑉))
44 simp2 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑎 = + )
4544oveqd 7172 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑤𝑎𝑥) = (𝑤 + 𝑥))
4645oveq2d 7171 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟𝑠(𝑤 + 𝑥)))
4744oveqd 7172 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)))
4846, 47eqeq12d 2837 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥))))
4944oveqd 7172 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))
5049eqeq2d 2832 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))))
5143, 48, 503anbi123d 1432 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))))
5220fveq2d 6673 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = (1r𝐹))
53 islmod.u . . . . . . . . . . . . . . . . . . . 20 1 = (1r𝐹)
5452, 53syl6eqr 2874 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = 1 )
5554oveq1d 7170 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((1r𝑓)𝑠𝑤) = ( 1 𝑠𝑤))
5655eqeq1d 2823 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((1r𝑓)𝑠𝑤) = 𝑤 ↔ ( 1 𝑠𝑤) = 𝑤))
5756anbi2d 630 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))
5851, 57anbi12d 632 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
5942, 58raleqbidv 3401 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6042, 59raleqbidv 3401 . . . . . . . . . . . . 13 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
61602ralbidv 3199 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6241, 61anbi12d 632 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6340, 62syl5bb 285 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6430, 63bitrd 281 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6526, 64sbceqbid 3778 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6623, 65sbceqbid 3778 . . . . . . 7 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6766sbcbidv 3826 . . . . . 6 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6817, 18, 19, 67sbc3ie 3851 . . . . 5 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6911fvexi 6683 . . . . . 6 · ∈ V
7022fvexi 6683 . . . . . 6 𝐾 ∈ V
7125fvexi 6683 . . . . . 6 ∈ V
72 simp2 1133 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑘 = 𝐾)
73 simp1 1132 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑠 = · )
7473oveqd 7172 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑤) = (𝑟 · 𝑤))
7574eleq1d 2897 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
7673oveqd 7172 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠(𝑤 + 𝑥)) = (𝑟 · (𝑤 + 𝑥)))
7773oveqd 7172 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
7874, 77oveq12d 7173 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
7976, 78eqeq12d 2837 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
80 simp3 1134 . . . . . . . . . . . . . . . 16 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑝 = )
8180oveqd 7172 . . . . . . . . . . . . . . 15 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑝𝑟) = (𝑞 𝑟))
8281oveq1d 7170 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟)𝑠𝑤))
8373oveqd 7172 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
8482, 83eqtrd 2856 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
8573oveqd 7172 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠𝑤) = (𝑞 · 𝑤))
8685, 74oveq12d 7173 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
8784, 86eqeq12d 2837 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) ↔ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
8875, 79, 873anbi123d 1432 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
8973oveqd 7172 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 × 𝑟)𝑠𝑤) = ((𝑞 × 𝑟) · 𝑤))
9074oveq2d 7171 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞𝑠(𝑟 · 𝑤)))
9173oveqd 7172 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟 · 𝑤)) = (𝑞 · (𝑟 · 𝑤)))
9290, 91eqtrd 2856 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞 · (𝑟 · 𝑤)))
9389, 92eqeq12d 2837 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
9473oveqd 7172 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 1 𝑠𝑤) = ( 1 · 𝑤))
9594eqeq1d 2823 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (( 1 𝑠𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
9693, 95anbi12d 632 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
9788, 96anbi12d 632 . . . . . . . . . 10 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
98972ralbidv 3199 . . . . . . . . 9 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
9972, 98raleqbidv 3401 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10072, 99raleqbidv 3401 . . . . . . 7 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
101100anbi2d 630 . . . . . 6 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
10269, 70, 71, 101sbc3ie 3851 . . . . 5 ([ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10368, 102bitri 277 . . . 4 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10416, 103syl6bb 289 . . 3 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
105 df-lmod 19635 . . 3 LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
106104, 105elrab2 3682 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
107 3anass 1091 . 2 ((𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))) ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
108106, 107bitr4i 280 1 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  w3a 1083   = wceq 1533  wcel 2110  wral 3138  [wsbc 3771  cfv 6354  (class class class)co 7155  Basecbs 16482  +gcplusg 16564  .rcmulr 16565  Scalarcsca 16567   ·𝑠 cvsca 16568  Grpcgrp 18102  1rcur 19250  Ringcrg 19296  LModclmod 19633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5209
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-iota 6313  df-fv 6362  df-ov 7158  df-lmod 19635
This theorem is referenced by:  lmodlema  19638  islmodd  19639  lmodgrp  19640  lmodring  19641  lmodprop2d  19695  isclmp  23700  lmodslmd  30832  ccfldsrarelvec  31056  lmod1  44548
  Copyright terms: Public domain W3C validator