Theorem lspsolvlem 19142

Description: Lemma for lspsolv 19143. (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 3687	. . . . . . 7 ⊢ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)} ⊆ 𝑉
4	2, 3	eqsstri 3635	. . . . . 6 ⊢ 𝑄 ⊆ 𝑉
5	4	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑄 ⊆ 𝑉)
6		lspsolv.ss	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ 𝑉)
7	1	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑊 ∈ LMod)
8		lspsolv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (Scalar‘𝑊)
9		lspsolv.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐹)
10		eqid 2622	. . . . . . . . . . 11 ⊢ (0g‘𝐹) = (0g‘𝐹)
11	8, 9, 10	lmod0cl 18889	. . . . . . . . . 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 2622	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝑊) = (0g‘𝑊)
17	14, 8, 15, 10, 16	lmod0vs 18896	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
18	1, 13, 17	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
19	18	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊))
20	19	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) = (𝑧 + (0g‘𝑊)))
21	6	sselda 3603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝑉)
22		lspsolv.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑊)
23	14, 22, 16	lmod0vrid 18894	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉) → (𝑧 + (0g‘𝑊)) = 𝑧)
24	7, 21, 23	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + (0g‘𝑊)) = 𝑧)
25	20, 24	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) = 𝑧)
26		lspsolv.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (LSpan‘𝑊)
27	14, 26	lspssid 18985	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → 𝐴 ⊆ (𝑁‘𝐴))
28	1, 6, 27	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ (𝑁‘𝐴))
29	28	sselda 3603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ (𝑁‘𝐴))
30	25, 29	eqeltrd 2701	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴))
31		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑟 = (0g‘𝐹) → (𝑟 · 𝑌) = ((0g‘𝐹) · 𝑌))
32	31	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑟 = (0g‘𝐹) → (𝑧 + (𝑟 · 𝑌)) = (𝑧 + ((0g‘𝐹) · 𝑌)))
33	32	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑟 = (0g‘𝐹) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴)))
34	33	rspcev 3309	. . . . . . . . 9 ⊢ (((0g‘𝐹) ∈ 𝐵 ∧ (𝑧 + ((0g‘𝐹) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
35	12, 30, 34	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
36	6, 35	ssrabdv 3681	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)})
37	36, 2	syl6sseqr 3652	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ 𝑄)
38	8	lmodfgrp 18872	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)
39	1, 38	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Grp)
40		eqid 2622	. . . . . . . . . . . 12 ⊢ (1r‘𝐹) = (1r‘𝐹)
41	8, 9, 40	lmod1cl 18890	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LMod → (1r‘𝐹) ∈ 𝐵)
42	1, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐹) ∈ 𝐵)
43		eqid 2622	. . . . . . . . . . 11 ⊢ (invg‘𝐹) = (invg‘𝐹)
44	9, 43	grpinvcl 17467	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Grp ∧ (1r‘𝐹) ∈ 𝐵) → ((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵)
45	39, 42, 44	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → ((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵)
46		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (invg‘𝑊) = (invg‘𝑊)
47	14, 46, 8, 15, 40, 43	lmodvneg1 18906	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌))
48	1, 13, 47	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌))
49	48	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (𝑌 + ((invg‘𝑊)‘𝑌)))
50		lmodgrp 18870	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
51	1, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ∈ Grp)
52	14, 22, 16, 46	grprinv 17469	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → (𝑌 + ((invg‘𝑊)‘𝑌)) = (0g‘𝑊))
53	51, 13, 52	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 + ((invg‘𝑊)‘𝑌)) = (0g‘𝑊))
54	49, 53	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (0g‘𝑊))
55		lspsolv.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (LSubSp‘𝑊)
56	14, 55, 26	lspcl 18976	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → (𝑁‘𝐴) ∈ 𝑆)
57	1, 6, 56	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘𝐴) ∈ 𝑆)
58	16, 55	lss0cl 18947	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LMod ∧ (𝑁‘𝐴) ∈ 𝑆) → (0g‘𝑊) ∈ (𝑁‘𝐴))
59	1, 57, 58	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑊) ∈ (𝑁‘𝐴))
60	54, 59	eqeltrd 2701	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴))
61		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑟 · 𝑌) = (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌))
62	61	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑌 + (𝑟 · 𝑌)) = (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)))
63	62	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → ((𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)))
64	63	rspcev 3309	. . . . . . . . 9 ⊢ ((((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵 ∧ (𝑌 + (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
65	45, 60, 64	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
66		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑌 → (𝑧 + (𝑟 · 𝑌)) = (𝑌 + (𝑟 · 𝑌)))
67	66	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑧 = 𝑌 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
68	67	rexbidv 3052	. . . . . . . . 9 ⊢ (𝑧 = 𝑌 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
69	68, 2	elrab2 3366	. . . . . . . 8 ⊢ (𝑌 ∈ 𝑄 ↔ (𝑌 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
70	13, 65, 69	sylanbrc 698	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑄)
71	70	snssd 4340	. . . . . 6 ⊢ (𝜑 → {𝑌} ⊆ 𝑄)
72	37, 71	unssd 3789	. . . . 5 ⊢ (𝜑 → (𝐴 ∪ {𝑌}) ⊆ 𝑄)
73	14, 26	lspss 18984	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑄 ⊆ 𝑉 ∧ (𝐴 ∪ {𝑌}) ⊆ 𝑄) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁‘𝑄))
74	1, 5, 72, 73	syl3anc 1326	. . . 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 3921	. . . . . . 7 ⊢ (𝑌 ∈ 𝑄 → 𝑄 ≠ ∅)
82	70, 81	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑄 ≠ ∅)
83		oveq1 6657	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (𝑧 + (𝑟 · 𝑌)) = (𝑥 + (𝑟 · 𝑌)))
84	83	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
85	84	rexbidv 3052	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
86		oveq1 6657	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑠 → (𝑟 · 𝑌) = (𝑠 · 𝑌))
87	86	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑠 → (𝑥 + (𝑟 · 𝑌)) = (𝑥 + (𝑠 · 𝑌)))
88	87	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → ((𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
89	88	cbvrexv 3172	. . . . . . . . . . . . 13 ⊢ (∃𝑟 ∈ 𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))
90	85, 89	syl6bb 276	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
91	90, 2	elrab2 3366	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑄 ↔ (𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)))
92		oveq1 6657	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑟 · 𝑌)) = (𝑦 + (𝑟 · 𝑌)))
93	92	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
94	93	rexbidv 3052	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
95		oveq1 6657	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑟 · 𝑌) = (𝑡 · 𝑌))
96	95	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑡 → (𝑦 + (𝑟 · 𝑌)) = (𝑦 + (𝑡 · 𝑌)))
97	96	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑡 → ((𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
98	97	cbvrexv 3172	. . . . . . . . . . . . 13 ⊢ (∃𝑟 ∈ 𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))
99	94, 98	syl6bb 276	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
100	99, 2	elrab2 3366	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝑄 ↔ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
101	91, 100	anbi12i 733	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
102		an4 865	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
103	101, 102	bitri 264	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))))
104		reeanv 3107	. . . . . . . . . . 11 ⊢ (∃𝑠 ∈ 𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) ↔ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))
105		simp1ll 1124	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝜑)
106	105, 1	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑊 ∈ LMod)
107		simp1lr 1125	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑎 ∈ 𝐵)
108		simp1rl 1126	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑥 ∈ 𝑉)
109	14, 8, 15, 9	lmodvscl 18880	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉) → (𝑎 · 𝑥) ∈ 𝑉)
110	106, 107, 108, 109	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · 𝑥) ∈ 𝑉)
111		simp1rr 1127	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑦 ∈ 𝑉)
112	14, 22	lmodvacl 18877	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
113	106, 110, 111, 112	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
114		simp2l 1087	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑠 ∈ 𝐵)
115		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐹) = (.r‘𝐹)
116	8, 9, 115	lmodmcl 18875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵)
117	106, 107, 114, 116	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵)
118		simp2r 1088	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑡 ∈ 𝐵)
119		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐹) = (+g‘𝐹)
120	8, 9, 119	lmodacl 18874	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ (𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵)
121	106, 117, 118, 120	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵)
122	105, 13	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑌 ∈ 𝑉)
123	14, 8, 15, 9	lmodvscl 18880	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑠 · 𝑌) ∈ 𝑉)
124	106, 114, 122, 123	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑠 · 𝑌) ∈ 𝑉)
125	14, 8, 15, 9	lmodvscl 18880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ (𝑠 · 𝑌) ∈ 𝑉) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
126	106, 107, 124, 125	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
127	14, 8, 15, 9	lmodvscl 18880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑡 · 𝑌) ∈ 𝑉)
128	106, 118, 122, 127	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑡 · 𝑌) ∈ 𝑉)
129	14, 22	lmod4 18913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ ((𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝑎 · (𝑠 · 𝑌)) ∈ 𝑉 ∧ (𝑡 · 𝑌) ∈ 𝑉)) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
130	106, 110, 111, 126, 128, 129	syl122anc 1335	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
131	14, 22, 8, 15, 9, 119	lmodvsdir 18887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ ((𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
132	106, 117, 118, 122, 131	syl13anc 1328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
133	14, 8, 15, 9, 115	lmodvsass 18888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
134	106, 107, 114, 122, 133	syl13anc 1328	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
135	134	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
136	132, 135	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
137	136	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))))
138	14, 22, 8, 15, 9	lmodvsdi 18886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ (𝑠 · 𝑌) ∈ 𝑉)) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
139	106, 107, 108, 124, 138	syl13anc 1328	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
140	139	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
141	130, 137, 140	3eqtr4d 2666	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
142	105, 57	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘𝐴) ∈ 𝑆)
143		simp3l 1089	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))
144		simp3r 1090	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))
145	8, 9, 22, 15, 55	lsscl 18943	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁‘𝐴) ∈ 𝑆 ∧ (𝑎 ∈ 𝐵 ∧ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴))
146	142, 107, 143, 144, 145	syl13anc 1328	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴))
147	141, 146	eqeltrd 2701	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴))
148		oveq1 6657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (𝑟 · 𝑌) = (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌))
149	148	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)))
150	149	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → ((((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)))
151	150	rspcev 3309	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵 ∧ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
152	121, 147, 151	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
153		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (𝑧 + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)))
154	153	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
155	154	rexbidv 3052	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
156	155, 2	elrab2 3366	. . . . . . . . . . . . . 14 ⊢ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑄 ↔ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
157	113, 152, 156	sylanbrc 698	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
158	157	3exp 1264	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)))
159	158	rexlimdvv 3037	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑠 ∈ 𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
160	104, 159	syl5bir 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
161	160	expimpd 629	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
162	103, 161	syl5bi 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
163	162	exp4b 632	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ 𝐵 → (𝑥 ∈ 𝑄 → (𝑦 ∈ 𝑄 → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))))
164	163	3imp2 1282	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
165	75, 76, 77, 78, 79, 80, 5, 82, 164	islssd 18936	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ 𝑆)
166	55, 26	lspid 18982	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆) → (𝑁‘𝑄) = 𝑄)
167	1, 165, 166	syl2anc 693	. . . 4 ⊢ (𝜑 → (𝑁‘𝑄) = 𝑄)
168	74, 167	sseqtrd 3641	. . 3 ⊢ (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑄)
169		lspsolv.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))
170	168, 169	sseldd 3604	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑄)
171		oveq1 6657	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑧 + (𝑟 · 𝑌)) = (𝑋 + (𝑟 · 𝑌)))
172	171	eleq1d 2686	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
173	172	rexbidv 3052	. . . 4 ⊢ (𝑧 = 𝑋 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
174	173, 2	elrab2 3366	. . 3 ⊢ (𝑋 ∈ 𝑄 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)))
175	174	simprbi 480	. 2 ⊢ (𝑋 ∈ 𝑄 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))
176	170, 175	syl 17	1 ⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913  {crab 2916   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  {csn 4177  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  +_gcplusg 15941  ._rcmulr 15942  Scalarcsca 15944   ·_𝑠 cvsca 15945  0_gc0g 16100  Grpcgrp 17422  inv_gcminusg 17423  1_rcur 18501  LModclmod 18863  LSubSpclss 18932  LSpanclspn 18971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-plusg 15954  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426  df-sbg 17427  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-lmod 18865  df-lss 18933  df-lsp 18972

This theorem is referenced by:  lspsolv  19143