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

Theorem lspsolvlem 19344
Description: Lemma for lspsolv 19345. (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.
StepHypRef Expression
1 lspsolv.w . . . . 5 (𝜑𝑊 ∈ LMod)
2 lspsolv.q . . . . . . 7 𝑄 = {𝑧𝑉 ∣ ∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)}
3 ssrab2 3878 . . . . . . 7 {𝑧𝑉 ∣ ∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)} ⊆ 𝑉
42, 3eqsstri 3826 . . . . . 6 𝑄𝑉
54a1i 11 . . . . 5 (𝜑𝑄𝑉)
6 lspsolv.ss . . . . . . . 8 (𝜑𝐴𝑉)
71adantr 468 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑊 ∈ LMod)
8 lspsolv.f . . . . . . . . . . 11 𝐹 = (Scalar‘𝑊)
9 lspsolv.b . . . . . . . . . . 11 𝐵 = (Base‘𝐹)
10 eqid 2802 . . . . . . . . . . 11 (0g𝐹) = (0g𝐹)
118, 9, 10lmod0cl 19087 . . . . . . . . . 10 (𝑊 ∈ LMod → (0g𝐹) ∈ 𝐵)
127, 11syl 17 . . . . . . . . 9 ((𝜑𝑧𝐴) → (0g𝐹) ∈ 𝐵)
13 lspsolv.y . . . . . . . . . . . . . 14 (𝜑𝑌𝑉)
14 lspsolv.v . . . . . . . . . . . . . . 15 𝑉 = (Base‘𝑊)
15 lspsolv.t . . . . . . . . . . . . . . 15 · = ( ·𝑠𝑊)
16 eqid 2802 . . . . . . . . . . . . . . 15 (0g𝑊) = (0g𝑊)
1714, 8, 15, 10, 16lmod0vs 19094 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → ((0g𝐹) · 𝑌) = (0g𝑊))
181, 13, 17syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → ((0g𝐹) · 𝑌) = (0g𝑊))
1918adantr 468 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → ((0g𝐹) · 𝑌) = (0g𝑊))
2019oveq2d 6884 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (𝑧 + ((0g𝐹) · 𝑌)) = (𝑧 + (0g𝑊)))
216sselda 3792 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → 𝑧𝑉)
22 lspsolv.p . . . . . . . . . . . . 13 + = (+g𝑊)
2314, 22, 16lmod0vrid 19092 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝑧𝑉) → (𝑧 + (0g𝑊)) = 𝑧)
247, 21, 23syl2anc 575 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (𝑧 + (0g𝑊)) = 𝑧)
2520, 24eqtrd 2836 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑧 + ((0g𝐹) · 𝑌)) = 𝑧)
26 lspsolv.n . . . . . . . . . . . . 13 𝑁 = (LSpan‘𝑊)
2714, 26lspssid 19186 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝐴𝑉) → 𝐴 ⊆ (𝑁𝐴))
281, 6, 27syl2anc 575 . . . . . . . . . . 11 (𝜑𝐴 ⊆ (𝑁𝐴))
2928sselda 3792 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑧 ∈ (𝑁𝐴))
3025, 29eqeltrd 2881 . . . . . . . . 9 ((𝜑𝑧𝐴) → (𝑧 + ((0g𝐹) · 𝑌)) ∈ (𝑁𝐴))
31 oveq1 6875 . . . . . . . . . . . 12 (𝑟 = (0g𝐹) → (𝑟 · 𝑌) = ((0g𝐹) · 𝑌))
3231oveq2d 6884 . . . . . . . . . . 11 (𝑟 = (0g𝐹) → (𝑧 + (𝑟 · 𝑌)) = (𝑧 + ((0g𝐹) · 𝑌)))
3332eleq1d 2866 . . . . . . . . . 10 (𝑟 = (0g𝐹) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑧 + ((0g𝐹) · 𝑌)) ∈ (𝑁𝐴)))
3433rspcev 3498 . . . . . . . . 9 (((0g𝐹) ∈ 𝐵 ∧ (𝑧 + ((0g𝐹) · 𝑌)) ∈ (𝑁𝐴)) → ∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
3512, 30, 34syl2anc 575 . . . . . . . 8 ((𝜑𝑧𝐴) → ∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
366, 35ssrabdv 3872 . . . . . . 7 (𝜑𝐴 ⊆ {𝑧𝑉 ∣ ∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)})
3736, 2syl6sseqr 3843 . . . . . 6 (𝜑𝐴𝑄)
388lmodfgrp 19070 . . . . . . . . . . 11 (𝑊 ∈ LMod → 𝐹 ∈ Grp)
391, 38syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ Grp)
40 eqid 2802 . . . . . . . . . . . 12 (1r𝐹) = (1r𝐹)
418, 9, 40lmod1cl 19088 . . . . . . . . . . 11 (𝑊 ∈ LMod → (1r𝐹) ∈ 𝐵)
421, 41syl 17 . . . . . . . . . 10 (𝜑 → (1r𝐹) ∈ 𝐵)
43 eqid 2802 . . . . . . . . . . 11 (invg𝐹) = (invg𝐹)
449, 43grpinvcl 17666 . . . . . . . . . 10 ((𝐹 ∈ Grp ∧ (1r𝐹) ∈ 𝐵) → ((invg𝐹)‘(1r𝐹)) ∈ 𝐵)
4539, 42, 44syl2anc 575 . . . . . . . . 9 (𝜑 → ((invg𝐹)‘(1r𝐹)) ∈ 𝐵)
46 eqid 2802 . . . . . . . . . . . . . 14 (invg𝑊) = (invg𝑊)
4714, 46, 8, 15, 40, 43lmodvneg1 19104 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → (((invg𝐹)‘(1r𝐹)) · 𝑌) = ((invg𝑊)‘𝑌))
481, 13, 47syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (((invg𝐹)‘(1r𝐹)) · 𝑌) = ((invg𝑊)‘𝑌))
4948oveq2d 6884 . . . . . . . . . . 11 (𝜑 → (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)) = (𝑌 + ((invg𝑊)‘𝑌)))
50 lmodgrp 19068 . . . . . . . . . . . . 13 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
511, 50syl 17 . . . . . . . . . . . 12 (𝜑𝑊 ∈ Grp)
5214, 22, 16, 46grprinv 17668 . . . . . . . . . . . 12 ((𝑊 ∈ Grp ∧ 𝑌𝑉) → (𝑌 + ((invg𝑊)‘𝑌)) = (0g𝑊))
5351, 13, 52syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((invg𝑊)‘𝑌)) = (0g𝑊))
5449, 53eqtrd 2836 . . . . . . . . . 10 (𝜑 → (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)) = (0g𝑊))
55 lspsolv.s . . . . . . . . . . . . 13 𝑆 = (LSubSp‘𝑊)
5614, 55, 26lspcl 19177 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝐴𝑉) → (𝑁𝐴) ∈ 𝑆)
571, 6, 56syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝑁𝐴) ∈ 𝑆)
5816, 55lss0cl 19145 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ (𝑁𝐴) ∈ 𝑆) → (0g𝑊) ∈ (𝑁𝐴))
591, 57, 58syl2anc 575 . . . . . . . . . 10 (𝜑 → (0g𝑊) ∈ (𝑁𝐴))
6054, 59eqeltrd 2881 . . . . . . . . 9 (𝜑 → (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)) ∈ (𝑁𝐴))
61 oveq1 6875 . . . . . . . . . . . 12 (𝑟 = ((invg𝐹)‘(1r𝐹)) → (𝑟 · 𝑌) = (((invg𝐹)‘(1r𝐹)) · 𝑌))
6261oveq2d 6884 . . . . . . . . . . 11 (𝑟 = ((invg𝐹)‘(1r𝐹)) → (𝑌 + (𝑟 · 𝑌)) = (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)))
6362eleq1d 2866 . . . . . . . . . 10 (𝑟 = ((invg𝐹)‘(1r𝐹)) → ((𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)) ∈ (𝑁𝐴)))
6463rspcev 3498 . . . . . . . . 9 ((((invg𝐹)‘(1r𝐹)) ∈ 𝐵 ∧ (𝑌 + (((invg𝐹)‘(1r𝐹)) · 𝑌)) ∈ (𝑁𝐴)) → ∃𝑟𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
6545, 60, 64syl2anc 575 . . . . . . . 8 (𝜑 → ∃𝑟𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
66 oveq1 6875 . . . . . . . . . . 11 (𝑧 = 𝑌 → (𝑧 + (𝑟 · 𝑌)) = (𝑌 + (𝑟 · 𝑌)))
6766eleq1d 2866 . . . . . . . . . 10 (𝑧 = 𝑌 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
6867rexbidv 3236 . . . . . . . . 9 (𝑧 = 𝑌 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑟𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
6968, 2elrab2 3558 . . . . . . . 8 (𝑌𝑄 ↔ (𝑌𝑉 ∧ ∃𝑟𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
7013, 65, 69sylanbrc 574 . . . . . . 7 (𝜑𝑌𝑄)
7170snssd 4524 . . . . . 6 (𝜑 → {𝑌} ⊆ 𝑄)
7237, 71unssd 3982 . . . . 5 (𝜑 → (𝐴 ∪ {𝑌}) ⊆ 𝑄)
7314, 26lspss 19185 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑄𝑉 ∧ (𝐴 ∪ {𝑌}) ⊆ 𝑄) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁𝑄))
741, 5, 72, 73syl3anc 1483 . . . 4 (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁𝑄))
758a1i 11 . . . . . 6 (𝜑𝐹 = (Scalar‘𝑊))
769a1i 11 . . . . . 6 (𝜑𝐵 = (Base‘𝐹))
7714a1i 11 . . . . . 6 (𝜑𝑉 = (Base‘𝑊))
7822a1i 11 . . . . . 6 (𝜑+ = (+g𝑊))
7915a1i 11 . . . . . 6 (𝜑· = ( ·𝑠𝑊))
8055a1i 11 . . . . . 6 (𝜑𝑆 = (LSubSp‘𝑊))
8170ne0d 4117 . . . . . 6 (𝜑𝑄 ≠ ∅)
82 oveq1 6875 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → (𝑧 + (𝑟 · 𝑌)) = (𝑥 + (𝑟 · 𝑌)))
8382eleq1d 2866 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
8483rexbidv 3236 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑟𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
85 oveq1 6875 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → (𝑟 · 𝑌) = (𝑠 · 𝑌))
8685oveq2d 6884 . . . . . . . . . . . . . . 15 (𝑟 = 𝑠 → (𝑥 + (𝑟 · 𝑌)) = (𝑥 + (𝑠 · 𝑌)))
8786eleq1d 2866 . . . . . . . . . . . . . 14 (𝑟 = 𝑠 → ((𝑥 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴)))
8887cbvrexv 3357 . . . . . . . . . . . . 13 (∃𝑟𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴))
8984, 88syl6bb 278 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴)))
9089, 2elrab2 3558 . . . . . . . . . . 11 (𝑥𝑄 ↔ (𝑥𝑉 ∧ ∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴)))
91 oveq1 6875 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑧 + (𝑟 · 𝑌)) = (𝑦 + (𝑟 · 𝑌)))
9291eleq1d 2866 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
9392rexbidv 3236 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑟𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
94 oveq1 6875 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑡 → (𝑟 · 𝑌) = (𝑡 · 𝑌))
9594oveq2d 6884 . . . . . . . . . . . . . . 15 (𝑟 = 𝑡 → (𝑦 + (𝑟 · 𝑌)) = (𝑦 + (𝑡 · 𝑌)))
9695eleq1d 2866 . . . . . . . . . . . . . 14 (𝑟 = 𝑡 → ((𝑦 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)))
9796cbvrexv 3357 . . . . . . . . . . . . 13 (∃𝑟𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))
9893, 97syl6bb 278 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)))
9998, 2elrab2 3558 . . . . . . . . . . 11 (𝑦𝑄 ↔ (𝑦𝑉 ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)))
10090, 99anbi12i 614 . . . . . . . . . 10 ((𝑥𝑄𝑦𝑄) ↔ ((𝑥𝑉 ∧ ∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴)) ∧ (𝑦𝑉 ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))))
101 an4 638 . . . . . . . . . 10 (((𝑥𝑉 ∧ ∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴)) ∧ (𝑦𝑉 ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) ↔ ((𝑥𝑉𝑦𝑉) ∧ (∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))))
102100, 101bitri 266 . . . . . . . . 9 ((𝑥𝑄𝑦𝑄) ↔ ((𝑥𝑉𝑦𝑉) ∧ (∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))))
103 reeanv 3291 . . . . . . . . . . 11 (∃𝑠𝐵𝑡𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)) ↔ (∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)))
104 simp1ll 1310 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝜑)
105104, 1syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑊 ∈ LMod)
106 simp1lr 1311 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑎𝐵)
107 simp1rl 1312 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑥𝑉)
10814, 8, 15, 9lmodvscl 19078 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑎𝐵𝑥𝑉) → (𝑎 · 𝑥) ∈ 𝑉)
109105, 106, 107, 108syl3anc 1483 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑎 · 𝑥) ∈ 𝑉)
110 simp1rr 1313 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑦𝑉)
11114, 22lmodvacl 19075 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ (𝑎 · 𝑥) ∈ 𝑉𝑦𝑉) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
112105, 109, 110, 111syl3anc 1483 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉)
113 simp2l 1249 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑠𝐵)
114 eqid 2802 . . . . . . . . . . . . . . . . . 18 (.r𝐹) = (.r𝐹)
1158, 9, 114lmodmcl 19073 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ LMod ∧ 𝑎𝐵𝑠𝐵) → (𝑎(.r𝐹)𝑠) ∈ 𝐵)
116105, 106, 113, 115syl3anc 1483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑎(.r𝐹)𝑠) ∈ 𝐵)
117 simp2r 1250 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑡𝐵)
118 eqid 2802 . . . . . . . . . . . . . . . . 17 (+g𝐹) = (+g𝐹)
1198, 9, 118lmodacl 19072 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ (𝑎(.r𝐹)𝑠) ∈ 𝐵𝑡𝐵) → ((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) ∈ 𝐵)
120105, 116, 117, 119syl3anc 1483 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) ∈ 𝐵)
121104, 13syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → 𝑌𝑉)
12214, 8, 15, 9lmodvscl 19078 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ LMod ∧ 𝑠𝐵𝑌𝑉) → (𝑠 · 𝑌) ∈ 𝑉)
123105, 113, 121, 122syl3anc 1483 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑠 · 𝑌) ∈ 𝑉)
12414, 8, 15, 9lmodvscl 19078 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ LMod ∧ 𝑎𝐵 ∧ (𝑠 · 𝑌) ∈ 𝑉) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
125105, 106, 123, 124syl3anc 1483 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉)
12614, 8, 15, 9lmodvscl 19078 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ LMod ∧ 𝑡𝐵𝑌𝑉) → (𝑡 · 𝑌) ∈ 𝑉)
127105, 117, 121, 126syl3anc 1483 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑡 · 𝑌) ∈ 𝑉)
12814, 22lmod4 19111 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ LMod ∧ ((𝑎 · 𝑥) ∈ 𝑉𝑦𝑉) ∧ ((𝑎 · (𝑠 · 𝑌)) ∈ 𝑉 ∧ (𝑡 · 𝑌) ∈ 𝑉)) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
129105, 109, 110, 125, 127, 128syl122anc 1491 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
13014, 22, 8, 15, 9, 118lmodvsdir 19085 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ LMod ∧ ((𝑎(.r𝐹)𝑠) ∈ 𝐵𝑡𝐵𝑌𝑉)) → (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌) = (((𝑎(.r𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
131105, 116, 117, 121, 130syl13anc 1484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌) = (((𝑎(.r𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)))
13214, 8, 15, 9, 114lmodvsass 19086 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ LMod ∧ (𝑎𝐵𝑠𝐵𝑌𝑉)) → ((𝑎(.r𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
133105, 106, 113, 121, 132syl13anc 1484 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎(.r𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌)))
134133oveq1d 6883 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎(.r𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
135131, 134eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))
136135oveq2d 6884 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))))
13714, 22, 8, 15, 9lmodvsdi 19084 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ LMod ∧ (𝑎𝐵𝑥𝑉 ∧ (𝑠 · 𝑌) ∈ 𝑉)) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
138105, 106, 107, 123, 137syl13anc 1484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))))
139138oveq1d 6883 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
140129, 136, 1393eqtr4d 2846 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)) = ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))))
141104, 57syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑁𝐴) ∈ 𝑆)
142 simp3l 1251 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴))
143 simp3r 1252 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))
1448, 9, 22, 15, 55lsscl 19141 . . . . . . . . . . . . . . . . 17 (((𝑁𝐴) ∈ 𝑆 ∧ (𝑎𝐵 ∧ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁𝐴))
145141, 106, 142, 143, 144syl13anc 1484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁𝐴))
146140, 145eqeltrd 2881 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)) ∈ (𝑁𝐴))
147 oveq1 6875 . . . . . . . . . . . . . . . . . 18 (𝑟 = ((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) → (𝑟 · 𝑌) = (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌))
148147oveq2d 6884 . . . . . . . . . . . . . . . . 17 (𝑟 = ((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) → (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)))
149148eleq1d 2866 . . . . . . . . . . . . . . . 16 (𝑟 = ((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) → ((((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)) ∈ (𝑁𝐴)))
150149rspcev 3498 . . . . . . . . . . . . . . 15 ((((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) ∈ 𝐵 ∧ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r𝐹)𝑠)(+g𝐹)𝑡) · 𝑌)) ∈ (𝑁𝐴)) → ∃𝑟𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
151120, 146, 150syl2anc 575 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ∃𝑟𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
152 oveq1 6875 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (𝑧 + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)))
153152eleq1d 2866 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝑎 · 𝑥) + 𝑦) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
154153rexbidv 3236 . . . . . . . . . . . . . . 15 (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑟𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
155154, 2elrab2 3558 . . . . . . . . . . . . . 14 (((𝑎 · 𝑥) + 𝑦) ∈ 𝑄 ↔ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑉 ∧ ∃𝑟𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
156112, 151, 155sylanbrc 574 . . . . . . . . . . . . 13 ((((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝑠𝐵𝑡𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
1571563exp 1141 . . . . . . . . . . . 12 (((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) → ((𝑠𝐵𝑡𝐵) → (((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)))
158157rexlimdvv 3221 . . . . . . . . . . 11 (((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) → (∃𝑠𝐵𝑡𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
159103, 158syl5bir 234 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ (𝑥𝑉𝑦𝑉)) → ((∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
160159expimpd 443 . . . . . . . . 9 ((𝜑𝑎𝐵) → (((𝑥𝑉𝑦𝑉) ∧ (∃𝑠𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁𝐴) ∧ ∃𝑡𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
161102, 160syl5bi 233 . . . . . . . 8 ((𝜑𝑎𝐵) → ((𝑥𝑄𝑦𝑄) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))
162161exp4b 419 . . . . . . 7 (𝜑 → (𝑎𝐵 → (𝑥𝑄 → (𝑦𝑄 → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))))
1631623imp2 1451 . . . . . 6 ((𝜑 ∧ (𝑎𝐵𝑥𝑄𝑦𝑄)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)
16475, 76, 77, 78, 79, 80, 5, 81, 163islssd 19134 . . . . 5 (𝜑𝑄𝑆)
16555, 26lspid 19183 . . . . 5 ((𝑊 ∈ LMod ∧ 𝑄𝑆) → (𝑁𝑄) = 𝑄)
1661, 164, 165syl2anc 575 . . . 4 (𝜑 → (𝑁𝑄) = 𝑄)
16774, 166sseqtrd 3832 . . 3 (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑄)
168 lspsolv.x . . 3 (𝜑𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌})))
169167, 168sseldd 3793 . 2 (𝜑𝑋𝑄)
170 oveq1 6875 . . . . . 6 (𝑧 = 𝑋 → (𝑧 + (𝑟 · 𝑌)) = (𝑋 + (𝑟 · 𝑌)))
171170eleq1d 2866 . . . . 5 (𝑧 = 𝑋 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
172171rexbidv 3236 . . . 4 (𝑧 = 𝑋 → (∃𝑟𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁𝐴) ↔ ∃𝑟𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
173172, 2elrab2 3558 . . 3 (𝑋𝑄 ↔ (𝑋𝑉 ∧ ∃𝑟𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁𝐴)))
174173simprbi 486 . 2 (𝑋𝑄 → ∃𝑟𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
175169, 174syl 17 1 (𝜑 → ∃𝑟𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2155  wrex 3093  {crab 3096  cun 3761  wss 3763  {csn 4364  cfv 6095  (class class class)co 6868  Basecbs 16062  +gcplusg 16147  .rcmulr 16148  Scalarcsca 16150   ·𝑠 cvsca 16151  0gc0g 16299  Grpcgrp 17621  invgcminusg 17622  1rcur 18697  LModclmod 19061  LSubSpclss 19130  LSpanclspn 19172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-er 7973  df-en 8187  df-dom 8188  df-sdom 8189  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-nn 11300  df-2 11358  df-ndx 16065  df-slot 16066  df-base 16068  df-sets 16069  df-plusg 16160  df-0g 16301  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-grp 17624  df-minusg 17625  df-sbg 17626  df-cmn 18390  df-abl 18391  df-mgp 18686  df-ur 18698  df-ring 18745  df-lmod 19063  df-lss 19131  df-lsp 19173
This theorem is referenced by:  lspsolv  19345
  Copyright terms: Public domain W3C validator