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

Theorem islmod 19185
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 6411 . . . . . 6 (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
2 islmod.v . . . . . 6 𝑉 = (Base‘𝑊)
31, 2syl6eqr 2851 . . . . 5 (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
4 fveq2 6411 . . . . . . 7 (𝑔 = 𝑊 → (+g𝑔) = (+g𝑊))
5 islmod.a . . . . . . 7 + = (+g𝑊)
64, 5syl6eqr 2851 . . . . . 6 (𝑔 = 𝑊 → (+g𝑔) = + )
7 fveq2 6411 . . . . . . . 8 (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
8 islmod.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
97, 8syl6eqr 2851 . . . . . . 7 (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
10 fveq2 6411 . . . . . . . . 9 (𝑔 = 𝑊 → ( ·𝑠𝑔) = ( ·𝑠𝑊))
11 islmod.s . . . . . . . . 9 · = ( ·𝑠𝑊)
1210, 11syl6eqr 2851 . . . . . . . 8 (𝑔 = 𝑊 → ( ·𝑠𝑔) = · )
1312sbceq1d 3638 . . . . . . 7 (𝑔 = 𝑊 → ([( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
149, 13sbceqbid 3640 . . . . . 6 (𝑔 = 𝑊 → ([(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
156, 14sbceqbid 3640 . . . . 5 (𝑔 = 𝑊 → ([(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
163, 15sbceqbid 3640 . . . 4 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
172fvexi 6425 . . . . . 6 𝑉 ∈ V
185fvexi 6425 . . . . . 6 + ∈ V
198fvexi 6425 . . . . . 6 𝐹 ∈ V
20 simp3 1169 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑓 = 𝐹)
2120fveq2d 6415 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
22 islmod.k . . . . . . . . 9 𝐾 = (Base‘𝐹)
2321, 22syl6eqr 2851 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
2420fveq2d 6415 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = (+g𝐹))
25 islmod.p . . . . . . . . . 10 = (+g𝐹)
2624, 25syl6eqr 2851 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = )
2720fveq2d 6415 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = (.r𝐹))
28 islmod.t . . . . . . . . . . . 12 × = (.r𝐹)
2927, 28syl6eqr 2851 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = × )
3029sbceq1d 3638 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
3128fvexi 6425 . . . . . . . . . . . 12 × ∈ V
32 oveq 6884 . . . . . . . . . . . . . . . . . . 19 (𝑡 = × → (𝑞𝑡𝑟) = (𝑞 × 𝑟))
3332oveq1d 6893 . . . . . . . . . . . . . . . . . 18 (𝑡 = × → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞 × 𝑟)𝑠𝑤))
3433eqeq1d 2801 . . . . . . . . . . . . . . . . 17 (𝑡 = × → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
3534anbi1d 624 . . . . . . . . . . . . . . . 16 (𝑡 = × → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
3635anbi2d 623 . . . . . . . . . . . . . . 15 (𝑡 = × → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
37362ralbidv 3170 . . . . . . . . . . . . . 14 (𝑡 = × → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
38372ralbidv 3170 . . . . . . . . . . . . 13 (𝑡 = × → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
3938anbi2d 623 . . . . . . . . . . . 12 (𝑡 = × → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
4031, 39sbcie 3668 . . . . . . . . . . 11 ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
4120eleq1d 2863 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑓 ∈ Ring ↔ 𝐹 ∈ Ring))
42 simp1 1167 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑣 = 𝑉)
4342eleq2d 2864 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟𝑠𝑤) ∈ 𝑉))
44 simp2 1168 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑎 = + )
4544oveqd 6895 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑤𝑎𝑥) = (𝑤 + 𝑥))
4645oveq2d 6894 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟𝑠(𝑤 + 𝑥)))
4744oveqd 6895 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)))
4846, 47eqeq12d 2814 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥))))
4944oveqd 6895 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))
5049eqeq2d 2809 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))))
5143, 48, 503anbi123d 1561 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))))
5220fveq2d 6415 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = (1r𝐹))
53 islmod.u . . . . . . . . . . . . . . . . . . . 20 1 = (1r𝐹)
5452, 53syl6eqr 2851 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = 1 )
5554oveq1d 6893 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((1r𝑓)𝑠𝑤) = ( 1 𝑠𝑤))
5655eqeq1d 2801 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((1r𝑓)𝑠𝑤) = 𝑤 ↔ ( 1 𝑠𝑤) = 𝑤))
5756anbi2d 623 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))
5851, 57anbi12d 625 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
5942, 58raleqbidv 3335 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6042, 59raleqbidv 3335 . . . . . . . . . . . . 13 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
61602ralbidv 3170 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6241, 61anbi12d 625 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6340, 62syl5bb 275 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6430, 63bitrd 271 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6526, 64sbceqbid 3640 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6623, 65sbceqbid 3640 . . . . . . 7 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6766sbcbidv 3688 . . . . . 6 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6817, 18, 19, 67sbc3ie 3703 . . . . 5 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6911fvexi 6425 . . . . . 6 · ∈ V
7022fvexi 6425 . . . . . 6 𝐾 ∈ V
7125fvexi 6425 . . . . . 6 ∈ V
72 simp2 1168 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑘 = 𝐾)
73 simp1 1167 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑠 = · )
7473oveqd 6895 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑤) = (𝑟 · 𝑤))
7574eleq1d 2863 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
7673oveqd 6895 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠(𝑤 + 𝑥)) = (𝑟 · (𝑤 + 𝑥)))
7773oveqd 6895 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
7874, 77oveq12d 6896 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
7976, 78eqeq12d 2814 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
80 simp3 1169 . . . . . . . . . . . . . . . 16 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑝 = )
8180oveqd 6895 . . . . . . . . . . . . . . 15 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑝𝑟) = (𝑞 𝑟))
8281oveq1d 6893 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟)𝑠𝑤))
8373oveqd 6895 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
8482, 83eqtrd 2833 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
8573oveqd 6895 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠𝑤) = (𝑞 · 𝑤))
8685, 74oveq12d 6896 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
8784, 86eqeq12d 2814 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) ↔ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
8875, 79, 873anbi123d 1561 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
8973oveqd 6895 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 × 𝑟)𝑠𝑤) = ((𝑞 × 𝑟) · 𝑤))
9074oveq2d 6894 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞𝑠(𝑟 · 𝑤)))
9173oveqd 6895 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟 · 𝑤)) = (𝑞 · (𝑟 · 𝑤)))
9290, 91eqtrd 2833 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞 · (𝑟 · 𝑤)))
9389, 92eqeq12d 2814 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
9473oveqd 6895 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 1 𝑠𝑤) = ( 1 · 𝑤))
9594eqeq1d 2801 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (( 1 𝑠𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
9693, 95anbi12d 625 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
9788, 96anbi12d 625 . . . . . . . . . 10 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
98972ralbidv 3170 . . . . . . . . 9 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
9972, 98raleqbidv 3335 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10072, 99raleqbidv 3335 . . . . . . 7 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
101100anbi2d 623 . . . . . 6 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
10269, 70, 71, 101sbc3ie 3703 . . . . 5 ([ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10368, 102bitri 267 . . . 4 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10416, 103syl6bb 279 . . 3 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
105 df-lmod 19183 . . 3 LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
106104, 105elrab2 3560 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
107 3anass 1117 . 2 ((𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))) ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
108106, 107bitr4i 270 1 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wral 3089  [wsbc 3633  cfv 6101  (class class class)co 6878  Basecbs 16184  +gcplusg 16267  .rcmulr 16268  Scalarcsca 16270   ·𝑠 cvsca 16271  Grpcgrp 17738  1rcur 18817  Ringcrg 18863  LModclmod 19181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-lmod 19183
This theorem is referenced by:  lmodlema  19186  islmodd  19187  lmodgrp  19188  lmodring  19189  lmodprop2d  19243  isclmp  23224  lmodslmd  30273  lmod1  43080
  Copyright terms: Public domain W3C validator