Theorem lspsolvlem 18963

Description: Lemma for lspsolv 18964. (Contributed by Mario Carneiro, 25-Jun-2014.)

Hypotheses

Ref	Expression
lspsolv.v	⊢ 𝑉 = (Base‘𝑊)
lspsolv.s	⊢ 𝑆 = (LSubSp‘𝑊)
lspsolv.n	⊢ 𝑁 = (LSpan‘𝑊)
lspsolv.f	⊢ 𝐹 = (Scalar‘𝑊)
lspsolv.b	⊢ 𝐵 = (Base‘𝐹)
lspsolv.p	⊢ + = (+g‘𝑊)
lspsolv.t	⊢ · = ( ·𝑠 ‘𝑊)
lspsolv.q	⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)}
lspsolv.w	⊢ (𝜑 → 𝑊 ∈ LMod)
lspsolv.ss	⊢ (𝜑 → 𝐴 ⊆ 𝑉)
lspsolv.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
lspsolv.x	⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))

Assertion

Ref	Expression
lspsolvlem	⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))

Distinct variable groups:   𝑧,𝑟,𝐴   𝐵,𝑟,𝑧   𝑁,𝑟,𝑧   𝜑,𝑧   𝐹,𝑟   𝑆,𝑟   𝑉,𝑟,𝑧   𝑊,𝑟,𝑧   + ,𝑟,𝑧   · ,𝑟,𝑧   𝑋,𝑟,𝑧   𝑌,𝑟,𝑧

Allowed substitution hints:   𝜑(𝑟)   𝑄(𝑧,𝑟)   𝑆(𝑧)   𝐹(𝑧)

Proof of Theorem lspsolvlem

Dummy variables 𝑠 𝑡 𝑥 𝑦 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lspsolv.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ LMod)
2		lspsolv.q	. . . . . . 7 ⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)}
3		ssrab2 3650	. . . . . . 7 ⊢ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)} ⊆ 𝑉
4	2, 3	eqsstri 3598	. . . . . 6 ⊢ 𝑄 ⊆ 𝑉
5	4	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
6		lspsolv.ss	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ 𝑉)
7	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑊 ∈ LMod)
8		lspsolv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (Scalar‘𝑊)
9		lspsolv.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐹)
10		eqid 2610	. . . . . . . . . . 11 ⊢ (0g‘𝐹) = (0g‘𝐹)
11	8, 9, 10	lmod0cl 18712	. . . . . . . . . 10 ⊢ (𝑊 ∈ LMod → (0g‘𝐹) ∈ 𝐵)
12	7, 11	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (0g‘𝐹) ∈ 𝐵)
13		lspsolv.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
14		lspsolv.v	. . . . . . . . . . . . . . 15 ⊢ 𝑉 = (Base‘𝑊)
15		lspsolv.t	. . . . . . . . . . . . . . 15 ⊢ · = ( ·𝑠 ‘𝑊)
16		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝑊) = (0g‘𝑊)
17	14, 8, 15, 10, 16	lmod0vs 18719	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
18	1, 13, 17	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
19	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
20	19	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) = (𝑧 + (0g‘𝑊)))
21	6	sselda 3568	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝑉)
22		lspsolv.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑊)
23	14, 22, 16	lmod0vrid 18717	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉) → (𝑧 + (0g‘𝑊)) = 𝑧)
24	7, 21, 23	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + (0g‘𝑊)) = 𝑧)
25	20, 24	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) = 𝑧)
26		lspsolv.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (LSpan‘𝑊)
27	14, 26	lspssid 18806	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → 𝐴 ⊆ (𝑁‘𝐴))
28	1, 6, 27	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ (𝑁‘𝐴))
29	28	sselda 3568	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ (𝑁‘𝐴))
30	25, 29	eqeltrd 2688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴))
31		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑟 = (0g‘𝐹) → (𝑟 · 𝑌) = ((0g‘𝐹) · 𝑌))
32	31	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑟 = (0g‘𝐹) → (𝑧 + (𝑟 · 𝑌)) = (𝑧 + ((0g‘𝐹) · 𝑌)))
33	32	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑟 = (0g‘𝐹) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴)))
34	33	rspcev 3282	. . . . . . . . 9 ⊢ (((0g‘𝐹) ∈ 𝐵 ∧ (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
35	12, 30, 34	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
36	6, 35	ssrabdv 3644	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)})
37	36, 2	syl6sseqr 3615	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ 𝑄)
38	8	lmodfgrp 18695	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)
39	1, 38	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Grp)
40		eqid 2610	. . . . . . . . . . . 12 ⊢ (1r‘𝐹) = (1r‘𝐹)
41	8, 9, 40	lmod1cl 18713	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LMod → (1r‘𝐹) ∈ 𝐵)
42	1, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐹) ∈ 𝐵)
43		eqid 2610	. . . . . . . . . . 11 ⊢ (invg‘𝐹) = (invg‘𝐹)
44	9, 43	grpinvcl 17290	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Grp ∧ (1r‘𝐹) ∈ 𝐵) → ((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵)
45	39, 42, 44	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵)
46		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (invg‘𝑊) = (invg‘𝑊)
47	14, 46, 8, 15, 40, 43	lmodvneg1 18729	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌))
48	1, 13, 47	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌))
49	48	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (𝑌 + ((invg‘𝑊)‘𝑌)))
50		lmodgrp 18693	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
51	1, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ∈ Grp)
52	14, 22, 16, 46	grprinv 17292	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → (𝑌 + ((invg‘𝑊)‘𝑌)) = (0g‘𝑊))
53	51, 13, 52	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((invg‘𝑊)‘𝑌)) = (0g‘𝑊))
54	49, 53	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (0g‘𝑊))
55		lspsolv.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (LSubSp‘𝑊)
56	14, 55, 26	lspcl 18797	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → (𝑁‘𝐴) ∈ 𝑆)
57	1, 6, 56	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘𝐴) ∈ 𝑆)
58	16, 55	lss0cl 18768	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LMod ∧ (𝑁‘𝐴) ∈ 𝑆) → (0g‘𝑊) ∈ (𝑁‘𝐴))
59	1, 57, 58	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑊) ∈ (𝑁‘𝐴))
60	54, 59	eqeltrd 2688	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴))
61		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑟 · 𝑌) = (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌))
62	61	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑌 + (𝑟 · 𝑌)) = (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)))
63	62	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → ((𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)))
64	63	rspcev 3282	. . . . . . . . 9 ⊢ ((((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵 ∧ (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
65	45, 60, 64	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
66		oveq1 6556	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑌 → (𝑧 + (𝑟 · 𝑌)) = (𝑌 + (𝑟 · 𝑌)))
67	66	eleq1d 2672	. . . . . . . . . 10 ⊢ (𝑧 = 𝑌 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
68	67	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑧 = 𝑌 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
69	68, 2	elrab2 3333	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑄 ↔ (𝑌 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
70	13, 65, 69	sylanbrc 695	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑄)
71	70	snssd 4281	. . . . . 6 ⊢ (𝜑 → {𝑌} ⊆ 𝑄)
72	37, 71	unssd 3751	. . . . 5 ⊢ (𝜑 → (𝐴 ∪ {𝑌}) ⊆ 𝑄)
73	14, 26	lspss 18805	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑄 ⊆ 𝑉 ∧ (𝐴 ∪ {𝑌}) ⊆ 𝑄) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁‘𝑄))
74	1, 5, 72, 73	syl3anc 1318	. . . 4 ⊢ (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁‘𝑄))
75	8	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))
76	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐹))
77	14	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑉 = (Base‘𝑊))
78	22	a1i 11	. . . . . 6 ⊢ (𝜑 → + = (+g‘𝑊))
79	15	a1i 11	. . . . . 6 ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))
80	55	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑆 = (LSubSp‘𝑊))
81		ne0i 3880	. . . . . . 7 ⊢ (𝑌 ∈ 𝑄 → 𝑄 ≠ ∅)
82	70, 81	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ≠ ∅)
83		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (𝑧 + (𝑟 · 𝑌)) = (𝑥 + (𝑟 · 𝑌)))
84	83	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
85	84	rexbidv 3034	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
86		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑠 → (𝑟 · 𝑌) = (𝑠 · 𝑌))
87	86	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑠 → (𝑥 + (𝑟 · 𝑌)) = (𝑥 + (𝑠 · 𝑌)))
88	87	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → ((𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
89	88	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑟 ∈ 𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))
90	85, 89	syl6bb 275	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
91	90, 2	elrab2 3333	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑄 ↔ (𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
92		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑟 · 𝑌)) = (𝑦 + (𝑟 · 𝑌)))
93	92	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
94	93	rexbidv 3034	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
95		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑟 · 𝑌) = (𝑡 · 𝑌))
96	95	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑡 → (𝑦 + (𝑟 · 𝑌)) = (𝑦 + (𝑡 · 𝑌)))
97	96	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑡 → ((𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
98	97	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑟 ∈ 𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))
99	94, 98	syl6bb 275	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
100	99, 2	elrab2 3333	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝑄 ↔ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
101	91, 100	anbi12i 729	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
102		an4 861	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
103	101, 102	bitri 263	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
104		reeanv 3086	. . . . . . . . . . 11 ⊢ (∃𝑠 ∈ 𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) ↔ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
105		simp1ll 1117	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝜑)
106	105, 1	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑊 ∈ LMod)
107		simp1lr 1118	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑎 ∈ 𝐵)
108		simp1rl 1119	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑥 ∈ 𝑉)
109	14, 8, 15, 9	lmodvscl 18703	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉) → (𝑎 · 𝑥) ∈ 𝑉)
110	106, 107, 108, 109	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · 𝑥) ∈ 𝑉)
111		simp1rr 1120	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑦 ∈ 𝑉)
112	14, 22	lmodvacl 18700	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
113	106, 110, 111, 112	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
114		simp2l 1080	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑠 ∈ 𝐵)
115		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐹) = (.r‘𝐹)
116	8, 9, 115	lmodmcl 18698	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵)
117	106, 107, 114, 116	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵)
118		simp2r 1081	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑡 ∈ 𝐵)
119		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐹) = (+g‘𝐹)
120	8, 9, 119	lmodacl 18697	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ (𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵)
121	106, 117, 118, 120	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵)
122	105, 13	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑌 ∈ 𝑉)
123	14, 8, 15, 9	lmodvscl 18703	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑠 · 𝑌) ∈ 𝑉)
124	106, 114, 122, 123	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑠 · 𝑌) ∈ 𝑉)
125	14, 8, 15, 9	lmodvscl 18703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ (𝑠 · 𝑌) ∈ 𝑉) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
126	106, 107, 124, 125	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
127	14, 8, 15, 9	lmodvscl 18703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑡 · 𝑌) ∈ 𝑉)
128	106, 118, 122, 127	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑡 · 𝑌) ∈ 𝑉)
129	14, 22	lmod4 18736	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ ((𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝑎 · (𝑠 · 𝑌)) ∈ 𝑉 ∧ (𝑡 · 𝑌) ∈ 𝑉)) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
130	106, 110, 111, 126, 128, 129	syl122anc 1327	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
131	14, 22, 8, 15, 9, 119	lmodvsdir 18710	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ ((𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
132	106, 117, 118, 122, 131	syl13anc 1320	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
133	14, 8, 15, 9, 115	lmodvsass 18711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
134	106, 107, 114, 122, 133	syl13anc 1320	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
135	134	oveq1d 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
136	132, 135	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
137	136	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))))
138	14, 22, 8, 15, 9	lmodvsdi 18709	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ (𝑠 · 𝑌) ∈ 𝑉)) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
139	106, 107, 108, 124, 138	syl13anc 1320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
140	139	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
141	130, 137, 140	3eqtr4d 2654	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
142	105, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘𝐴) ∈ 𝑆)
143		simp3l 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))
144		simp3r 1083	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))
145	8, 9, 22, 15, 55	lsscl 18764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁‘𝐴) ∈ 𝑆 ∧ (𝑎 ∈ 𝐵 ∧ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴))
146	142, 107, 143, 144, 145	syl13anc 1320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴))
147	141, 146	eqeltrd 2688	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴))
148		oveq1 6556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (𝑟 · 𝑌) = (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌))
149	148	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)))
150	149	eleq1d 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → ((((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)))
151	150	rspcev 3282	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵 ∧ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
152	121, 147, 151	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
153		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (𝑧 + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)))
154	153	eleq1d 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
155	154	rexbidv 3034	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
156	155, 2	elrab2 3333	. . . . . . . . . . . . . 14 ⊢ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑄 ↔ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
157	113, 152, 156	sylanbrc 695	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
158	157	3exp 1256	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)))
159	158	rexlimdvv 3019	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑠 ∈ 𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
160	104, 159	syl5bir 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
161	160	expimpd 627	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
162	103, 161	syl5bi 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
163	162	exp4b 630	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ 𝐵 → (𝑥 ∈ 𝑄 → (𝑦 ∈ 𝑄 → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))))
164	163	3imp2 1274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
165	75, 76, 77, 78, 79, 80, 5, 82, 164	islssd 18757	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ 𝑆)
166	55, 26	lspid 18803	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆) → (𝑁‘𝑄) = 𝑄)
167	1, 165, 166	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝑁‘𝑄) = 𝑄)
168	74, 167	sseqtrd 3604	. . 3 ⊢ (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑄)
169		lspsolv.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))
170	168, 169	sseldd 3569	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑄)
171		oveq1 6556	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 + (𝑟 · 𝑌)) = (𝑋 + (𝑟 · 𝑌)))
172	171	eleq1d 2672	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
173	172	rexbidv 3034	. . . 4 ⊢ (𝑧 = 𝑋 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
174	173, 2	elrab2 3333	. . 3 ⊢ (𝑋 ∈ 𝑄 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
175	174	simprbi 479	. 2 ⊢ (𝑋 ∈ 𝑄 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
176	170, 175	syl 17	1 ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {crab 2900   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  0_gc0g 15923  Grpcgrp 17245  inv_gcminusg 17246  1_rcur 18324  LModclmod 18686  LSubSpclss 18753  LSpanclspn 18792

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-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-plusg 15781  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-sbg 17250  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-lmod 18688  df-lss 18754  df-lsp 18793

This theorem is referenced by:  lspsolv  18964