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

Theorem islmod 19090
 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 6354 . . . . . 6 (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
2 islmod.v . . . . . 6 𝑉 = (Base‘𝑊)
31, 2syl6eqr 2813 . . . . 5 (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
4 fveq2 6354 . . . . . . 7 (𝑔 = 𝑊 → (+g𝑔) = (+g𝑊))
5 islmod.a . . . . . . 7 + = (+g𝑊)
64, 5syl6eqr 2813 . . . . . 6 (𝑔 = 𝑊 → (+g𝑔) = + )
7 fveq2 6354 . . . . . . . 8 (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
8 islmod.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
97, 8syl6eqr 2813 . . . . . . 7 (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
10 fveq2 6354 . . . . . . . . 9 (𝑔 = 𝑊 → ( ·𝑠𝑔) = ( ·𝑠𝑊))
11 islmod.s . . . . . . . . 9 · = ( ·𝑠𝑊)
1210, 11syl6eqr 2813 . . . . . . . 8 (𝑔 = 𝑊 → ( ·𝑠𝑔) = · )
1312sbceq1d 3582 . . . . . . 7 (𝑔 = 𝑊 → ([( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
149, 13sbceqbid 3584 . . . . . 6 (𝑔 = 𝑊 → ([(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
156, 14sbceqbid 3584 . . . . 5 (𝑔 = 𝑊 → ([(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
163, 15sbceqbid 3584 . . . 4 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
17 fvex 6364 . . . . . . 7 (Base‘𝑊) ∈ V
182, 17eqeltri 2836 . . . . . 6 𝑉 ∈ V
19 fvex 6364 . . . . . . 7 (+g𝑊) ∈ V
205, 19eqeltri 2836 . . . . . 6 + ∈ V
21 fvex 6364 . . . . . . 7 (Scalar‘𝑊) ∈ V
228, 21eqeltri 2836 . . . . . 6 𝐹 ∈ V
23 simp3 1133 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑓 = 𝐹)
2423fveq2d 6358 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
25 islmod.k . . . . . . . . 9 𝐾 = (Base‘𝐹)
2624, 25syl6eqr 2813 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
2723fveq2d 6358 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = (+g𝐹))
28 islmod.p . . . . . . . . . 10 = (+g𝐹)
2927, 28syl6eqr 2813 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (+g𝑓) = )
3023fveq2d 6358 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = (.r𝐹))
31 islmod.t . . . . . . . . . . . 12 × = (.r𝐹)
3230, 31syl6eqr 2813 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (.r𝑓) = × )
3332sbceq1d 3582 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
34 fvex 6364 . . . . . . . . . . . . 13 (.r𝐹) ∈ V
3531, 34eqeltri 2836 . . . . . . . . . . . 12 × ∈ V
36 oveq 6821 . . . . . . . . . . . . . . . . . . 19 (𝑡 = × → (𝑞𝑡𝑟) = (𝑞 × 𝑟))
3736oveq1d 6830 . . . . . . . . . . . . . . . . . 18 (𝑡 = × → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞 × 𝑟)𝑠𝑤))
3837eqeq1d 2763 . . . . . . . . . . . . . . . . 17 (𝑡 = × → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
3938anbi1d 743 . . . . . . . . . . . . . . . 16 (𝑡 = × → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
4039anbi2d 742 . . . . . . . . . . . . . . 15 (𝑡 = × → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
41402ralbidv 3128 . . . . . . . . . . . . . 14 (𝑡 = × → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
42412ralbidv 3128 . . . . . . . . . . . . 13 (𝑡 = × → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
4342anbi2d 742 . . . . . . . . . . . 12 (𝑡 = × → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))))
4435, 43sbcie 3612 . . . . . . . . . . 11 ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))))
4523eleq1d 2825 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑓 ∈ Ring ↔ 𝐹 ∈ Ring))
46 simp1 1131 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑣 = 𝑉)
4746eleq2d 2826 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟𝑠𝑤) ∈ 𝑉))
48 simp2 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → 𝑎 = + )
4948oveqd 6832 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑤𝑎𝑥) = (𝑤 + 𝑥))
5049oveq2d 6831 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟𝑠(𝑤 + 𝑥)))
5148oveqd 6832 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)))
5250, 51eqeq12d 2776 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥))))
5348oveqd 6832 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))
5453eqeq2d 2771 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))))
5547, 52, 543anbi123d 1548 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))))
5623fveq2d 6358 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = (1r𝐹))
57 islmod.u . . . . . . . . . . . . . . . . . . . 20 1 = (1r𝐹)
5856, 57syl6eqr 2813 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (1r𝑓) = 1 )
5958oveq1d 6830 . . . . . . . . . . . . . . . . . 18 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((1r𝑓)𝑠𝑤) = ( 1 𝑠𝑤))
6059eqeq1d 2763 . . . . . . . . . . . . . . . . 17 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (((1r𝑓)𝑠𝑤) = 𝑤 ↔ ( 1 𝑠𝑤) = 𝑤))
6160anbi2d 742 . . . . . . . . . . . . . . . 16 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))
6255, 61anbi12d 749 . . . . . . . . . . . . . . 15 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6346, 62raleqbidv 3292 . . . . . . . . . . . . . 14 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6446, 63raleqbidv 3292 . . . . . . . . . . . . 13 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
65642ralbidv 3128 . . . . . . . . . . . 12 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → (∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
6645, 65anbi12d 749 . . . . . . . . . . 11 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ((𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6744, 66syl5bb 272 . . . . . . . . . 10 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6833, 67bitrd 268 . . . . . . . . 9 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
6929, 68sbceqbid 3584 . . . . . . . 8 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
7026, 69sbceqbid 3584 . . . . . . 7 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
7170sbcbidv 3632 . . . . . 6 ((𝑣 = 𝑉𝑎 = +𝑓 = 𝐹) → ([ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
7218, 20, 22, 71sbc3ie 3649 . . . . 5 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
73 fvex 6364 . . . . . . 7 ( ·𝑠𝑊) ∈ V
7411, 73eqeltri 2836 . . . . . 6 · ∈ V
75 fvex 6364 . . . . . . 7 (Base‘𝐹) ∈ V
7625, 75eqeltri 2836 . . . . . 6 𝐾 ∈ V
77 fvex 6364 . . . . . . 7 (+g𝐹) ∈ V
7828, 77eqeltri 2836 . . . . . 6 ∈ V
79 simp2 1132 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑘 = 𝐾)
80 simp1 1131 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑠 = · )
8180oveqd 6832 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑤) = (𝑟 · 𝑤))
8281eleq1d 2825 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
8380oveqd 6832 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠(𝑤 + 𝑥)) = (𝑟 · (𝑤 + 𝑥)))
8480oveqd 6832 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
8581, 84oveq12d 6833 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
8683, 85eqeq12d 2776 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
87 simp3 1133 . . . . . . . . . . . . . . . 16 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → 𝑝 = )
8887oveqd 6832 . . . . . . . . . . . . . . 15 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑝𝑟) = (𝑞 𝑟))
8988oveq1d 6830 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟)𝑠𝑤))
9080oveqd 6832 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
9189, 90eqtrd 2795 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 𝑟) · 𝑤))
9280oveqd 6832 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠𝑤) = (𝑞 · 𝑤))
9392, 81oveq12d 6833 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
9491, 93eqeq12d 2776 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) ↔ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
9582, 86, 943anbi123d 1548 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
9680oveqd 6832 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝑞 × 𝑟)𝑠𝑤) = ((𝑞 × 𝑟) · 𝑤))
9781oveq2d 6831 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞𝑠(𝑟 · 𝑤)))
9880oveqd 6832 . . . . . . . . . . . . . 14 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟 · 𝑤)) = (𝑞 · (𝑟 · 𝑤)))
9997, 98eqtrd 2795 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞 · (𝑟 · 𝑤)))
10096, 99eqeq12d 2776 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
10180oveqd 6832 . . . . . . . . . . . . 13 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ( 1 𝑠𝑤) = ( 1 · 𝑤))
102101eqeq1d 2763 . . . . . . . . . . . 12 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (( 1 𝑠𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
103100, 102anbi12d 749 . . . . . . . . . . 11 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
10495, 103anbi12d 749 . . . . . . . . . 10 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
1051042ralbidv 3128 . . . . . . . . 9 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10679, 105raleqbidv 3292 . . . . . . . 8 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
10779, 106raleqbidv 3292 . . . . . . 7 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → (∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
108107anbi2d 742 . . . . . 6 ((𝑠 = ·𝑘 = 𝐾𝑝 = ) → ((𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
10974, 76, 78, 108sbc3ie 3649 . . . . 5 ([ · / 𝑠][𝐾 / 𝑘][ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑉𝑤𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
11072, 109bitri 264 . . . 4 ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
11116, 110syl6bb 276 . . 3 (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
112 df-lmod 19088 . . 3 LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
113111, 112elrab2 3508 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
114 3anass 1081 . 2 ((𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))) ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
115113, 114bitr4i 267 1 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2140  ∀wral 3051  Vcvv 3341  [wsbc 3577  ‘cfv 6050  (class class class)co 6815  Basecbs 16080  +gcplusg 16164  .rcmulr 16165  Scalarcsca 16167   ·𝑠 cvsca 16168  Grpcgrp 17644  1rcur 18722  Ringcrg 18768  LModclmod 19086 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-nul 4942 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-lmod 19088 This theorem is referenced by:  lmodlema  19091  islmodd  19092  lmodgrp  19093  lmodring  19094  lmodprop2d  19148  isclmp  23118  lmodslmd  30088  lmod1  42810
 Copyright terms: Public domain W3C validator