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

Theorem lspfixed 20198
Description: Show membership in the span of the sum of two vectors, one of which (𝑌) is fixed in advance. (Contributed by NM, 27-May-2015.) (Revised by AV, 12-Jul-2022.)
Hypotheses
Ref Expression
lspfixed.v 𝑉 = (Base‘𝑊)
lspfixed.p + = (+g𝑊)
lspfixed.o 0 = (0g𝑊)
lspfixed.n 𝑁 = (LSpan‘𝑊)
lspfixed.w (𝜑𝑊 ∈ LVec)
lspfixed.y (𝜑𝑌𝑉)
lspfixed.z (𝜑𝑍𝑉)
lspfixed.e (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
lspfixed.f (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍}))
lspfixed.g (𝜑𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
Assertion
Ref Expression
lspfixed (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
Distinct variable groups:   𝑧,𝑁   𝑧, 0   𝑧, +   𝑧,𝑊   𝑧,𝑋   𝑧,𝑌   𝑧,𝑍
Allowed substitution hints:   𝜑(𝑧)   𝑉(𝑧)

Proof of Theorem lspfixed
Dummy variables 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lspfixed.g . . 3 (𝜑𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
2 lspfixed.v . . . 4 𝑉 = (Base‘𝑊)
3 lspfixed.p . . . 4 + = (+g𝑊)
4 eqid 2739 . . . 4 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2739 . . . 4 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6 eqid 2739 . . . 4 ( ·𝑠𝑊) = ( ·𝑠𝑊)
7 lspfixed.n . . . 4 𝑁 = (LSpan‘𝑊)
8 lspfixed.w . . . . 5 (𝜑𝑊 ∈ LVec)
9 lveclmod 20176 . . . . 5 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
108, 9syl 17 . . . 4 (𝜑𝑊 ∈ LMod)
11 lspfixed.y . . . 4 (𝜑𝑌𝑉)
12 lspfixed.z . . . 4 (𝜑𝑍𝑉)
132, 3, 4, 5, 6, 7, 10, 11, 12lspprel 20164 . . 3 (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))))
141, 13mpbid 235 . 2 (𝜑 → ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))
15103ad2ant1 1135 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑊 ∈ LMod)
16 eqid 2739 . . . . . . . . . 10 (LSubSp‘𝑊) = (LSubSp‘𝑊)
172, 16, 7lspsncl 20047 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ 𝑍𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
1810, 12, 17syl2anc 587 . . . . . . . 8 (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
19183ad2ant1 1135 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
2083ad2ant1 1135 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑊 ∈ LVec)
214lvecdrng 20175 . . . . . . . . 9 (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ DivRing)
2220, 21syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (Scalar‘𝑊) ∈ DivRing)
23 simp2l 1201 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
24 lspfixed.f . . . . . . . . . 10 (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍}))
25243ad2ant1 1135 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ¬ 𝑋 ∈ (𝑁‘{𝑍}))
26 simpl3 1195 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))
27 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑘 = (0g‘(Scalar‘𝑊)))
2827oveq1d 7250 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑌) = ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌))
29 simpl1 1193 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝜑)
3029, 10syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑊 ∈ LMod)
3129, 11syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑌𝑉)
32 eqid 2739 . . . . . . . . . . . . . . . . 17 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
33 lspfixed.o . . . . . . . . . . . . . . . . 17 0 = (0g𝑊)
342, 4, 6, 32, 33lmod0vs 19965 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌) = 0 )
3530, 31, 34syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌) = 0 )
3628, 35eqtrd 2779 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑌) = 0 )
3736oveq1d 7250 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) = ( 0 + (𝑙( ·𝑠𝑊)𝑍)))
38 simp2r 1202 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑙 ∈ (Base‘(Scalar‘𝑊)))
39123ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑍𝑉)
402, 4, 6, 5lmodvscl 19949 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑍𝑉) → (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉)
4115, 38, 39, 40syl3anc 1373 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉)
4241adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉)
432, 3, 33lmod0vlid 19962 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉) → ( 0 + (𝑙( ·𝑠𝑊)𝑍)) = (𝑙( ·𝑠𝑊)𝑍))
4430, 42, 43syl2anc 587 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ( 0 + (𝑙( ·𝑠𝑊)𝑍)) = (𝑙( ·𝑠𝑊)𝑍))
4526, 37, 443eqtrd 2783 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑙( ·𝑠𝑊)𝑍))
4629, 18syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
47 simpl2r 1229 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑙 ∈ (Base‘(Scalar‘𝑊)))
482, 7lspsnid 20063 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑍𝑉) → 𝑍 ∈ (𝑁‘{𝑍}))
4910, 12, 48syl2anc 587 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑁‘{𝑍}))
5029, 49syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑍 ∈ (𝑁‘{𝑍}))
514, 6, 5, 16lssvscl 20025 . . . . . . . . . . . . 13 (((𝑊 ∈ LMod ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) ∧ (𝑙 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑍 ∈ (𝑁‘{𝑍}))) → (𝑙( ·𝑠𝑊)𝑍) ∈ (𝑁‘{𝑍}))
5230, 46, 47, 50, 51syl22anc 839 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠𝑊)𝑍) ∈ (𝑁‘{𝑍}))
5345, 52eqeltrd 2840 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑍}))
5453ex 416 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑘 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑍})))
5554necon3bd 2957 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑍}) → 𝑘 ≠ (0g‘(Scalar‘𝑊))))
5625, 55mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑘 ≠ (0g‘(Scalar‘𝑊)))
57 eqid 2739 . . . . . . . . 9 (invr‘(Scalar‘𝑊)) = (invr‘(Scalar‘𝑊))
585, 32, 57drnginvrcl 19817 . . . . . . . 8 (((Scalar‘𝑊) ∈ DivRing ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) → ((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)))
5922, 23, 56, 58syl3anc 1373 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)))
60493ad2ant1 1135 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑍 ∈ (𝑁‘{𝑍}))
6115, 19, 38, 60, 51syl22anc 839 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑙( ·𝑠𝑊)𝑍) ∈ (𝑁‘{𝑍}))
624, 6, 5, 16lssvscl 20025 . . . . . . 7 (((𝑊 ∈ LMod ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) ∧ (((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑙( ·𝑠𝑊)𝑍) ∈ (𝑁‘{𝑍}))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ (𝑁‘{𝑍}))
6315, 19, 59, 61, 62syl22anc 839 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ (𝑁‘{𝑍}))
645, 32, 57drnginvrn0 19818 . . . . . . . 8 (((Scalar‘𝑊) ∈ DivRing ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) → ((invr‘(Scalar‘𝑊))‘𝑘) ≠ (0g‘(Scalar‘𝑊)))
6522, 23, 56, 64syl3anc 1373 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((invr‘(Scalar‘𝑊))‘𝑘) ≠ (0g‘(Scalar‘𝑊)))
66 lspfixed.e . . . . . . . . . 10 (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
67663ad2ant1 1135 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ¬ 𝑋 ∈ (𝑁‘{𝑌}))
68 simpl3 1195 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))
69 oveq1 7242 . . . . . . . . . . . . . . 15 (𝑙 = (0g‘(Scalar‘𝑊)) → (𝑙( ·𝑠𝑊)𝑍) = ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑍))
702, 4, 6, 32, 33lmod0vs 19965 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑍𝑉) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑍) = 0 )
7115, 39, 70syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((0g‘(Scalar‘𝑊))( ·𝑠𝑊)𝑍) = 0 )
7269, 71sylan9eqr 2802 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠𝑊)𝑍) = 0 )
7372oveq2d 7251 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) = ((𝑘( ·𝑠𝑊)𝑌) + 0 ))
74113ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑌𝑉)
752, 4, 6, 5lmodvscl 19949 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌𝑉) → (𝑘( ·𝑠𝑊)𝑌) ∈ 𝑉)
7615, 23, 74, 75syl3anc 1373 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑘( ·𝑠𝑊)𝑌) ∈ 𝑉)
772, 3, 33lmod0vrid 19963 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ (𝑘( ·𝑠𝑊)𝑌) ∈ 𝑉) → ((𝑘( ·𝑠𝑊)𝑌) + 0 ) = (𝑘( ·𝑠𝑊)𝑌))
7815, 76, 77syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((𝑘( ·𝑠𝑊)𝑌) + 0 ) = (𝑘( ·𝑠𝑊)𝑌))
7978adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠𝑊)𝑌) + 0 ) = (𝑘( ·𝑠𝑊)𝑌))
8068, 73, 793eqtrd 2783 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑘( ·𝑠𝑊)𝑌))
812, 16, 7lspsncl 20047 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
8210, 11, 81syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
83823ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊))
842, 7lspsnid 20063 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → 𝑌 ∈ (𝑁‘{𝑌}))
8510, 11, 84syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (𝑁‘{𝑌}))
86853ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑌 ∈ (𝑁‘{𝑌}))
874, 6, 5, 16lssvscl 20025 . . . . . . . . . . . . . 14 (((𝑊 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ (𝑁‘{𝑌}))) → (𝑘( ·𝑠𝑊)𝑌) ∈ (𝑁‘{𝑌}))
8815, 83, 23, 86, 87syl22anc 839 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑘( ·𝑠𝑊)𝑌) ∈ (𝑁‘{𝑌}))
8988adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠𝑊)𝑌) ∈ (𝑁‘{𝑌}))
9080, 89eqeltrd 2840 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑌}))
9190ex 416 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑙 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑌})))
9291necon3bd 2957 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑌}) → 𝑙 ≠ (0g‘(Scalar‘𝑊))))
9367, 92mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑙 ≠ (0g‘(Scalar‘𝑊)))
94 simpl1 1193 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝜑)
9594, 1syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
96 preq2 4667 . . . . . . . . . . . . . 14 (𝑍 = 0 → {𝑌, 𝑍} = {𝑌, 0 })
9796fveq2d 6743 . . . . . . . . . . . . 13 (𝑍 = 0 → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌, 0 }))
982, 33, 7, 15, 74lsppr0 20162 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{𝑌, 0 }) = (𝑁‘{𝑌}))
9997, 98sylan9eqr 2802 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑍 = 0 ) → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌}))
10095, 99eleqtrd 2842 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌}))
101100ex 416 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑍 = 0𝑋 ∈ (𝑁‘{𝑌})))
102101necon3bd 2957 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑌}) → 𝑍0 ))
10367, 102mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑍0 )
1042, 6, 4, 5, 32, 33, 20, 38, 39lvecvsn0 20179 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((𝑙( ·𝑠𝑊)𝑍) ≠ 0 ↔ (𝑙 ≠ (0g‘(Scalar‘𝑊)) ∧ 𝑍0 )))
10593, 103, 104mpbir2and 713 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑙( ·𝑠𝑊)𝑍) ≠ 0 )
1062, 6, 4, 5, 32, 33, 20, 59, 41lvecvsn0 20179 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ≠ 0 ↔ (((invr‘(Scalar‘𝑊))‘𝑘) ≠ (0g‘(Scalar‘𝑊)) ∧ (𝑙( ·𝑠𝑊)𝑍) ≠ 0 )))
10765, 105, 106mpbir2and 713 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ≠ 0 )
108 eldifsn 4717 . . . . . 6 ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ↔ ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ (𝑁‘{𝑍}) ∧ (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ≠ 0 ))
10963, 107, 108sylanbrc 586 . . . . 5 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }))
110 simp3 1140 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))
1112, 3lmodvacl 19946 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ (𝑘( ·𝑠𝑊)𝑌) ∈ 𝑉 ∧ (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ 𝑉)
11215, 76, 41, 111syl3anc 1373 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ 𝑉)
1132, 7lspsnid 20063 . . . . . . . 8 ((𝑊 ∈ LMod ∧ ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ 𝑉) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}))
11415, 112, 113syl2anc 587 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}))
115110, 114eqeltrd 2840 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}))
1162, 4, 6, 5, 32, 7lspsnvs 20184 . . . . . . . 8 ((𝑊 ∈ LVec ∧ (((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ ((invr‘(Scalar‘𝑊))‘𝑘) ≠ (0g‘(Scalar‘𝑊))) ∧ ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) ∈ 𝑉) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))}) = (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}))
11720, 59, 65, 112, 116syl121anc 1377 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))}) = (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}))
1182, 3, 4, 6, 5lmodvsdi 19955 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ (((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘( ·𝑠𝑊)𝑌) ∈ 𝑉 ∧ (𝑙( ·𝑠𝑊)𝑍) ∈ 𝑉)) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) = ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)) + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))))
11915, 59, 76, 41, 118syl13anc 1374 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) = ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)) + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))))
120 eqid 2739 . . . . . . . . . . . . . . 15 (.r‘(Scalar‘𝑊)) = (.r‘(Scalar‘𝑊))
121 eqid 2739 . . . . . . . . . . . . . . 15 (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
1225, 32, 120, 121, 57drnginvrl 19819 . . . . . . . . . . . . . 14 (((Scalar‘𝑊) ∈ DivRing ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0g‘(Scalar‘𝑊))) → (((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘) = (1r‘(Scalar‘𝑊)))
12322, 23, 56, 122syl3anc 1373 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘) = (1r‘(Scalar‘𝑊)))
124123oveq1d 7250 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠𝑊)𝑌) = ((1r‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌))
1252, 4, 6, 5, 120lmodvsass 19957 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ (((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌𝑉)) → ((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠𝑊)𝑌) = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)))
12615, 59, 23, 74, 125syl13anc 1374 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠𝑊)𝑌) = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)))
1272, 4, 6, 121lmodvs1 19960 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ 𝑌𝑉) → ((1r‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌) = 𝑌)
12815, 74, 127syl2anc 587 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((1r‘(Scalar‘𝑊))( ·𝑠𝑊)𝑌) = 𝑌)
129124, 126, 1283eqtr3d 2787 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)) = 𝑌)
130129oveq1d 7250 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑘( ·𝑠𝑊)𝑌)) + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))) = (𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))))
131119, 130eqtrd 2779 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) = (𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))))
132131sneqd 4570 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → {(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))} = {(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))})
133132fveq2d 6743 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)))}) = (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))}))
134117, 133eqtr3d 2781 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → (𝑁‘{((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))}) = (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))}))
135115, 134eleqtrd 2842 . . . . 5 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))}))
136 oveq2 7243 . . . . . . . . 9 (𝑧 = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) → (𝑌 + 𝑧) = (𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍))))
137136sneqd 4570 . . . . . . . 8 (𝑧 = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) → {(𝑌 + 𝑧)} = {(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))})
138137fveq2d 6743 . . . . . . 7 (𝑧 = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) → (𝑁‘{(𝑌 + 𝑧)}) = (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))}))
139138eleq2d 2825 . . . . . 6 (𝑧 = (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) → (𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}) ↔ 𝑋 ∈ (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))})))
140139rspcev 3552 . . . . 5 (((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ∧ 𝑋 ∈ (𝑁‘{(𝑌 + (((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠𝑊)(𝑙( ·𝑠𝑊)𝑍)))})) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
141109, 135, 140syl2anc 587 . . . 4 ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍))) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
1421413exp 1121 . . 3 (𝜑 → ((𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) → (𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))))
143142rexlimdvv 3222 . 2 (𝜑 → (∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠𝑊)𝑌) + (𝑙( ·𝑠𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})))
14414, 143mpd 15 1 (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2112  wne 2943  wrex 3065  cdif 3880  {csn 4558  {cpr 4560  cfv 6401  (class class class)co 7235  Basecbs 16793  +gcplusg 16835  .rcmulr 16836  Scalarcsca 16838   ·𝑠 cvsca 16839  0gc0g 16977  1rcur 19549  invrcinvr 19722  DivRingcdr 19800  LModclmod 19932  LSubSpclss 20001  LSpanclspn 20041  LVecclvec 20172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-1st 7783  df-2nd 7784  df-tpos 7992  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-er 8415  df-en 8651  df-dom 8652  df-sdom 8653  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-nn 11861  df-2 11923  df-3 11924  df-sets 16750  df-slot 16768  df-ndx 16778  df-base 16794  df-ress 16818  df-plusg 16848  df-mulr 16849  df-0g 16979  df-mgm 18147  df-sgrp 18196  df-mnd 18207  df-submnd 18252  df-grp 18401  df-minusg 18402  df-sbg 18403  df-subg 18573  df-cntz 18744  df-lsm 19058  df-cmn 19205  df-abl 19206  df-mgp 19538  df-ur 19550  df-ring 19597  df-oppr 19674  df-dvdsr 19692  df-unit 19693  df-invr 19723  df-drng 19802  df-lmod 19934  df-lss 20002  df-lsp 20042  df-lvec 20173
This theorem is referenced by:  lsatfixedN  36797
  Copyright terms: Public domain W3C validator