Theorem islmod 18690

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.

Step	Hyp	Ref	Expression
1		fveq2 6103	. . . . . 6 ⊢ (𝑔 = 𝑊 → (Base‘𝑔) = (Base‘𝑊))
2		islmod.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
3	1, 2	syl6eqr 2662	. . . . 5 ⊢ (𝑔 = 𝑊 → (Base‘𝑔) = 𝑉)
4		fveq2 6103	. . . . . . 7 ⊢ (𝑔 = 𝑊 → (+g‘𝑔) = (+g‘𝑊))
5		islmod.a	. . . . . . 7 ⊢ + = (+g‘𝑊)
6	4, 5	syl6eqr 2662	. . . . . 6 ⊢ (𝑔 = 𝑊 → (+g‘𝑔) = + )
7		fveq2 6103	. . . . . . . 8 ⊢ (𝑔 = 𝑊 → (Scalar‘𝑔) = (Scalar‘𝑊))
8		islmod.f	. . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊)
9	7, 8	syl6eqr 2662	. . . . . . 7 ⊢ (𝑔 = 𝑊 → (Scalar‘𝑔) = 𝐹)
10		fveq2 6103	. . . . . . . . 9 ⊢ (𝑔 = 𝑊 → ( ·𝑠 ‘𝑔) = ( ·𝑠 ‘𝑊))
11		islmod.s	. . . . . . . . 9 ⊢ · = ( ·𝑠 ‘𝑊)
12	10, 11	syl6eqr 2662	. . . . . . . 8 ⊢ (𝑔 = 𝑊 → ( ·𝑠 ‘𝑔) = · )
13	12	sbceq1d 3407	. . . . . . 7 ⊢ (𝑔 = 𝑊 → ([( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
14	9, 13	sbceqbid 3409	. . . . . 6 ⊢ (𝑔 = 𝑊 → ([(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
15	6, 14	sbceqbid 3409	. . . . 5 ⊢ (𝑔 = 𝑊 → ([(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
16	3, 15	sbceqbid 3409	. . . 4 ⊢ (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
17		fvex 6113	. . . . . . 7 ⊢ (Base‘𝑊) ∈ V
18	2, 17	eqeltri 2684	. . . . . 6 ⊢ 𝑉 ∈ V
19		fvex 6113	. . . . . . 7 ⊢ (+g‘𝑊) ∈ V
20	5, 19	eqeltri 2684	. . . . . 6 ⊢ + ∈ V
21		fvex 6113	. . . . . . 7 ⊢ (Scalar‘𝑊) ∈ V
22	8, 21	eqeltri 2684	. . . . . 6 ⊢ 𝐹 ∈ V
23		simp3 1056	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
24	23	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
25		islmod.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝐹)
26	24, 25	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
27	23	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (+g‘𝑓) = (+g‘𝐹))
28		islmod.p	. . . . . . . . . 10 ⊢ ⨣ = (+g‘𝐹)
29	27, 28	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (+g‘𝑓) = ⨣ )
30	23	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (.r‘𝑓) = (.r‘𝐹))
31		islmod.t	. . . . . . . . . . . 12 ⊢ × = (.r‘𝐹)
32	30, 31	syl6eqr 2662	. . . . . . . . . . 11 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (.r‘𝑓) = × )
33	32	sbceq1d 3407	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
34		fvex 6113	. . . . . . . . . . . . 13 ⊢ (.r‘𝐹) ∈ V
35	31, 34	eqeltri 2684	. . . . . . . . . . . 12 ⊢ × ∈ V
36		oveq 6555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = × → (𝑞𝑡𝑟) = (𝑞 × 𝑟))
37	36	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = × → ((𝑞𝑡𝑟)𝑠𝑤) = ((𝑞 × 𝑟)𝑠𝑤))
38	37	eqeq1d 2612	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = × → (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))))
39	38	anbi1d 737	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = × → ((((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
40	39	anbi2d 736	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = × → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))))
41	40	2ralbidv 2972	. . . . . . . . . . . . . 14 ⊢ (𝑡 = × → (∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))))
42	41	2ralbidv 2972	. . . . . . . . . . . . 13 ⊢ (𝑡 = × → (∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))))
43	42	anbi2d 736	. . . . . . . . . . . 12 ⊢ (𝑡 = × → ((𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))))
44	35, 43	sbcie 3437	. . . . . . . . . . 11 ⊢ ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))))
45	23	eleq1d 2672	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (𝑓 ∈ Ring ↔ 𝐹 ∈ Ring))
46		simp1 1054	. . . . . . . . . . . . . 14 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → 𝑣 = 𝑉)
47	46	eleq2d 2673	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((𝑟𝑠𝑤) ∈ 𝑣 ↔ (𝑟𝑠𝑤) ∈ 𝑉))
48		simp2 1055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → 𝑎 = + )
49	48	oveqd 6566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (𝑤𝑎𝑥) = (𝑤 + 𝑥))
50	49	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (𝑟𝑠(𝑤𝑎𝑥)) = (𝑟𝑠(𝑤 + 𝑥)))
51	48	oveqd 6566	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)))
52	50, 51	eqeq12d 2625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ↔ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥))))
53	48	oveqd 6566	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))
54	53	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)) ↔ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))))
55	47, 52, 54	3anbi123d 1391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ↔ ((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)))))
56	23	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (1r‘𝑓) = (1r‘𝐹))
57		islmod.u	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 = (1r‘𝐹)
58	56, 57	syl6eqr 2662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (1r‘𝑓) = 1 )
59	58	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((1r‘𝑓)𝑠𝑤) = ( 1 𝑠𝑤))
60	59	eqeq1d 2612	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (((1r‘𝑓)𝑠𝑤) = 𝑤 ↔ ( 1 𝑠𝑤) = 𝑤))
61	60	anbi2d 736	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))
62	55, 61	anbi12d 743	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
63	46, 62	raleqbidv 3129	. . . . . . . . . . . . . 14 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
64	46, 63	raleqbidv 3129	. . . . . . . . . . . . 13 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
65	64	2ralbidv 2972	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → (∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)) ↔ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
66	45, 65	anbi12d 743	. . . . . . . . . . 11 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ((𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
67	44, 66	syl5bb 271	. . . . . . . . . 10 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([ × / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
68	33, 67	bitrd 267	. . . . . . . . 9 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
69	29, 68	sbceqbid 3409	. . . . . . . 8 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ ⨣ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
70	26, 69	sbceqbid 3409	. . . . . . 7 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [𝐾 / 𝑘][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
71	70	sbcbidv 3457	. . . . . 6 ⊢ ((𝑣 = 𝑉 ∧ 𝑎 = + ∧ 𝑓 = 𝐹) → ([ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)))))
72	18, 20, 22, 71	sbc3ie 3474	. . . . 5 ⊢ ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ [ · / 𝑠][𝐾 / 𝑘][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))))
73		fvex 6113	. . . . . . 7 ⊢ ( ·𝑠 ‘𝑊) ∈ V
74	11, 73	eqeltri 2684	. . . . . 6 ⊢ · ∈ V
75		fvex 6113	. . . . . . 7 ⊢ (Base‘𝐹) ∈ V
76	25, 75	eqeltri 2684	. . . . . 6 ⊢ 𝐾 ∈ V
77		fvex 6113	. . . . . . 7 ⊢ (+g‘𝐹) ∈ V
78	28, 77	eqeltri 2684	. . . . . 6 ⊢ ⨣ ∈ V
79		simp2 1055	. . . . . . . 8 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → 𝑘 = 𝐾)
80		simp1 1054	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → 𝑠 = · )
81	80	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑟𝑠𝑤) = (𝑟 · 𝑤))
82	81	eleq1d 2672	. . . . . . . . . . . 12 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑟𝑠𝑤) ∈ 𝑉 ↔ (𝑟 · 𝑤) ∈ 𝑉))
83	80	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑟𝑠(𝑤 + 𝑥)) = (𝑟 · (𝑤 + 𝑥)))
84	80	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑟𝑠𝑥) = (𝑟 · 𝑥))
85	81, 84	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)))
86	83, 85	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ↔ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥))))
87		simp3 1056	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → 𝑝 = ⨣ )
88	87	oveqd 6566	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑞𝑝𝑟) = (𝑞 ⨣ 𝑟))
89	88	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 ⨣ 𝑟)𝑠𝑤))
90	80	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑞 ⨣ 𝑟)𝑠𝑤) = ((𝑞 ⨣ 𝑟) · 𝑤))
91	89, 90	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞 ⨣ 𝑟) · 𝑤))
92	80	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑞𝑠𝑤) = (𝑞 · 𝑤))
93	92, 81	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))
94	91, 93	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤)) ↔ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))))
95	82, 86, 94	3anbi123d 1391	. . . . . . . . . . 11 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ↔ ((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤)))))
96	80	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝑞 × 𝑟)𝑠𝑤) = ((𝑞 × 𝑟) · 𝑤))
97	81	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞𝑠(𝑟 · 𝑤)))
98	80	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑞𝑠(𝑟 · 𝑤)) = (𝑞 · (𝑟 · 𝑤)))
99	97, 98	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (𝑞𝑠(𝑟𝑠𝑤)) = (𝑞 · (𝑟 · 𝑤)))
100	96, 99	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ↔ ((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤))))
101	80	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ( 1 𝑠𝑤) = ( 1 · 𝑤))
102	101	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (( 1 𝑠𝑤) = 𝑤 ↔ ( 1 · 𝑤) = 𝑤))
103	100, 102	anbi12d 743	. . . . . . . . . . 11 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤) ↔ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))
104	95, 103	anbi12d 743	. . . . . . . . . 10 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
105	104	2ralbidv 2972	. . . . . . . . 9 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
106	79, 105	raleqbidv 3129	. . . . . . . 8 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
107	79, 106	raleqbidv 3129	. . . . . . 7 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → (∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤)) ↔ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
108	107	anbi2d 736	. . . . . 6 ⊢ ((𝑠 = · ∧ 𝑘 = 𝐾 ∧ 𝑝 = ⨣ ) → ((𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
109	74, 76, 78, 108	sbc3ie 3474	. . . . 5 ⊢ ([ · / 𝑠][𝐾 / 𝑘][ ⨣ / 𝑝](𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟𝑠𝑤) ∈ 𝑉 ∧ (𝑟𝑠(𝑤 + 𝑥)) = ((𝑟𝑠𝑤) + (𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤) + (𝑟𝑠𝑤))) ∧ (((𝑞 × 𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ( 1 𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
110	72, 109	bitri 263	. . . 4 ⊢ ([𝑉 / 𝑣][ + / 𝑎][𝐹 / 𝑓][ · / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))
111	16, 110	syl6bb 275	. . 3 ⊢ (𝑔 = 𝑊 → ([(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))) ↔ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
112		df-lmod 18688	. . 3 ⊢ LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}
113	111, 112	elrab2 3333	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
114		3anass 1035	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))) ↔ (𝑊 ∈ Grp ∧ (𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤)))))
115	113, 114	bitr4i 266	1 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ 𝐾 ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑟 · 𝑤) ∈ 𝑉 ∧ (𝑟 · (𝑤 + 𝑥)) = ((𝑟 · 𝑤) + (𝑟 · 𝑥)) ∧ ((𝑞 ⨣ 𝑟) · 𝑤) = ((𝑞 · 𝑤) + (𝑟 · 𝑤))) ∧ (((𝑞 × 𝑟) · 𝑤) = (𝑞 · (𝑟 · 𝑤)) ∧ ( 1 · 𝑤) = 𝑤))))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173  [wsbc 3402  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  Grpcgrp 17245  1_rcur 18324  Ringcrg 18370  LModclmod 18686

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-lmod 18688

This theorem is referenced by:  lmodlema  18691  islmodd  18692  lmodgrp  18693  lmodring  18694  lmodprop2d  18748  isclmp  22705  lmodslmd  29088  lmod1  42075