| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lspfixed.g | . . 3
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) | 
| 2 |  | lspfixed.v | . . . 4
⊢ 𝑉 = (Base‘𝑊) | 
| 3 |  | lspfixed.p | . . . 4
⊢  + =
(+g‘𝑊) | 
| 4 |  | eqid 2737 | . . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 5 |  | eqid 2737 | . . . 4
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 6 |  | eqid 2737 | . . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 7 |  | lspfixed.n | . . . 4
⊢ 𝑁 = (LSpan‘𝑊) | 
| 8 |  | lspfixed.w | . . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) | 
| 9 |  | lveclmod 21105 | . . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | 
| 10 | 8, 9 | syl 17 | . . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 11 |  | lspfixed.y | . . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 12 |  | lspfixed.z | . . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑉) | 
| 13 | 2, 3, 4, 5, 6, 7, 10, 11, 12 | lspprel 21093 | . . 3
⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)))) | 
| 14 | 1, 13 | mpbid 232 | . 2
⊢ (𝜑 → ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) | 
| 15 | 10 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑊 ∈ LMod) | 
| 16 |  | eqid 2737 | . . . . . . . . . 10
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 17 | 2, 16, 7 | lspsncl 20975 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) | 
| 18 | 10, 12, 17 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) | 
| 19 | 18 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) | 
| 20 | 8 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑊 ∈ LVec) | 
| 21 | 4 | lvecdrng 21104 | . . . . . . . . 9
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
DivRing) | 
| 22 | 20, 21 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (Scalar‘𝑊) ∈ DivRing) | 
| 23 |  | simp2l 1200 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) | 
| 24 |  | lspfixed.f | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍})) | 
| 25 | 24 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ¬ 𝑋 ∈ (𝑁‘{𝑍})) | 
| 26 |  | simpl3 1194 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) | 
| 27 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑘 = (0g‘(Scalar‘𝑊))) | 
| 28 | 27 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) | 
| 29 |  | simpl1 1192 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝜑) | 
| 30 | 29, 10 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑊 ∈ LMod) | 
| 31 | 29, 11 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑌 ∈ 𝑉) | 
| 32 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 33 |  | lspfixed.o | . . . . . . . . . . . . . . . . 17
⊢  0 =
(0g‘𝑊) | 
| 34 | 2, 4, 6, 32, 33 | lmod0vs 20893 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 0 ) | 
| 35 | 30, 31, 34 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 0 ) | 
| 36 | 28, 35 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) = 0 ) | 
| 37 | 36 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) = ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍))) | 
| 38 |  | simp2r 1201 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑙 ∈ (Base‘(Scalar‘𝑊))) | 
| 39 | 12 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑍 ∈ 𝑉) | 
| 40 | 2, 4, 6, 5 | lmodvscl 20876 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑍 ∈ 𝑉) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) | 
| 41 | 15, 38, 39, 40 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) | 
| 43 | 2, 3, 33 | lmod0vlid 20890 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝑙(
·𝑠 ‘𝑊)𝑍) ∈ 𝑉) → ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍)) = (𝑙( ·𝑠
‘𝑊)𝑍)) | 
| 44 | 30, 42, 43 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍)) = (𝑙( ·𝑠
‘𝑊)𝑍)) | 
| 45 | 26, 37, 44 | 3eqtrd 2781 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑙( ·𝑠
‘𝑊)𝑍)) | 
| 46 | 29, 18 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) | 
| 47 |  | simpl2r 1228 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑙 ∈ (Base‘(Scalar‘𝑊))) | 
| 48 | 2, 7 | lspsnid 20991 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → 𝑍 ∈ (𝑁‘{𝑍})) | 
| 49 | 10, 12, 48 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑍})) | 
| 50 | 29, 49 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑍 ∈ (𝑁‘{𝑍})) | 
| 51 | 4, 6, 5, 16 | lssvscl 20953 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) ∧ (𝑙 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑍 ∈ (𝑁‘{𝑍}))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) | 
| 52 | 30, 46, 47, 50, 51 | syl22anc 839 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) | 
| 53 | 45, 52 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑍})) | 
| 54 | 53 | ex 412 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑍}))) | 
| 55 | 54 | necon3bd 2954 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑍}) → 𝑘 ≠
(0g‘(Scalar‘𝑊)))) | 
| 56 | 25, 55 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) | 
| 57 |  | eqid 2737 | . . . . . . . . 9
⊢
(invr‘(Scalar‘𝑊)) =
(invr‘(Scalar‘𝑊)) | 
| 58 | 5, 32, 57 | drnginvrcl 20753 | . . . . . . . 8
⊢
(((Scalar‘𝑊)
∈ DivRing ∧ 𝑘
∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) →
((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊))) | 
| 59 | 22, 23, 56, 58 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊))) | 
| 60 | 49 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑍 ∈ (𝑁‘{𝑍})) | 
| 61 | 15, 19, 38, 60, 51 | syl22anc 839 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) | 
| 62 | 4, 6, 5, 16 | lssvscl 20953 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) ∧
(((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍}))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ (𝑁‘{𝑍})) | 
| 63 | 15, 19, 59, 61, 62 | syl22anc 839 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ (𝑁‘{𝑍})) | 
| 64 | 5, 32, 57 | drnginvrn0 20754 | . . . . . . . 8
⊢
(((Scalar‘𝑊)
∈ DivRing ∧ 𝑘
∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) →
((invr‘(Scalar‘𝑊))‘𝑘) ≠
(0g‘(Scalar‘𝑊))) | 
| 65 | 22, 23, 56, 64 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((invr‘(Scalar‘𝑊))‘𝑘) ≠
(0g‘(Scalar‘𝑊))) | 
| 66 |  | lspfixed.e | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) | 
| 67 | 66 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ¬ 𝑋 ∈ (𝑁‘{𝑌})) | 
| 68 |  | simpl3 1194 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) | 
| 69 |  | oveq1 7438 | . . . . . . . . . . . . . . 15
⊢ (𝑙 =
(0g‘(Scalar‘𝑊)) → (𝑙( ·𝑠
‘𝑊)𝑍) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍)) | 
| 70 | 2, 4, 6, 32, 33 | lmod0vs 20893 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍) = 0 ) | 
| 71 | 15, 39, 70 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍) = 0 ) | 
| 72 | 69, 71 | sylan9eqr 2799 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) = 0 ) | 
| 73 | 72 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) = ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 )) | 
| 74 | 11 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑌 ∈ 𝑉) | 
| 75 | 2, 4, 6, 5 | lmodvscl 20876 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) | 
| 76 | 15, 23, 74, 75 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) | 
| 77 | 2, 3, 33 | lmod0vrid 20891 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) | 
| 78 | 15, 76, 77 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) | 
| 80 | 68, 73, 79 | 3eqtrd 2781 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑘( ·𝑠
‘𝑊)𝑌)) | 
| 81 | 2, 16, 7 | lspsncl 20975 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) | 
| 82 | 10, 11, 81 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) | 
| 83 | 82 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) | 
| 84 | 2, 7 | lspsnid 20991 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ (𝑁‘{𝑌})) | 
| 85 | 10, 11, 84 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑌})) | 
| 86 | 85 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑌 ∈ (𝑁‘{𝑌})) | 
| 87 | 4, 6, 5, 16 | lssvscl 20953 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ (𝑁‘{𝑌}))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) | 
| 88 | 15, 83, 23, 86, 87 | syl22anc 839 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) | 
| 90 | 80, 89 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑌})) | 
| 91 | 90 | ex 412 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑌}))) | 
| 92 | 91 | necon3bd 2954 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑌}) → 𝑙 ≠
(0g‘(Scalar‘𝑊)))) | 
| 93 | 67, 92 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑙 ≠
(0g‘(Scalar‘𝑊))) | 
| 94 |  | simpl1 1192 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝜑) | 
| 95 | 94, 1 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) | 
| 96 |  | preq2 4734 | . . . . . . . . . . . . . 14
⊢ (𝑍 = 0 → {𝑌, 𝑍} = {𝑌, 0 }) | 
| 97 | 96 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑍 = 0 → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌, 0 })) | 
| 98 | 2, 33, 7, 15, 74 | lsppr0 21091 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑌, 0 }) = (𝑁‘{𝑌})) | 
| 99 | 97, 98 | sylan9eqr 2799 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌})) | 
| 100 | 95, 99 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌})) | 
| 101 | 100 | ex 412 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑍 = 0 → 𝑋 ∈ (𝑁‘{𝑌}))) | 
| 102 | 101 | necon3bd 2954 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑌}) → 𝑍 ≠ 0 )) | 
| 103 | 67, 102 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑍 ≠ 0 ) | 
| 104 | 2, 6, 4, 5, 32, 33, 20, 38, 39 | lvecvsn0 21111 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑙( ·𝑠
‘𝑊)𝑍) ≠ 0 ↔ (𝑙 ≠
(0g‘(Scalar‘𝑊)) ∧ 𝑍 ≠ 0 ))) | 
| 105 | 93, 103, 104 | mpbir2and 713 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙( ·𝑠
‘𝑊)𝑍) ≠ 0 ) | 
| 106 | 2, 6, 4, 5, 32, 33, 20, 59, 41 | lvecvsn0 21111 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ≠ 0 ↔
(((invr‘(Scalar‘𝑊))‘𝑘) ≠
(0g‘(Scalar‘𝑊)) ∧ (𝑙( ·𝑠
‘𝑊)𝑍) ≠ 0 ))) | 
| 107 | 65, 105, 106 | mpbir2and 713 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ≠ 0 ) | 
| 108 |  | eldifsn 4786 | . . . . . 6
⊢
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ↔
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ (𝑁‘{𝑍}) ∧
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ≠ 0 )) | 
| 109 | 63, 107, 108 | sylanbrc 583 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 })) | 
| 110 |  | simp3 1139 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) | 
| 111 | 2, 3 | lmodvacl 20873 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉 ∧ (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) | 
| 112 | 15, 76, 41, 111 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) | 
| 113 | 2, 7 | lspsnid 20991 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) | 
| 114 | 15, 112, 113 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) | 
| 115 | 110, 114 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) | 
| 116 | 2, 4, 6, 5, 32, 7 | lspsnvs 21116 | . . . . . . . 8
⊢ ((𝑊 ∈ LVec ∧
(((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧
((invr‘(Scalar‘𝑊))‘𝑘) ≠
(0g‘(Scalar‘𝑊))) ∧ ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍)))}) = (𝑁‘{((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍))})) | 
| 117 | 20, 59, 65, 112, 116 | syl121anc 1377 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍)))}) = (𝑁‘{((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍))})) | 
| 118 | 2, 3, 4, 6, 5 | lmodvsdi 20883 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧
(((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘( ·𝑠
‘𝑊)𝑌) ∈ 𝑉 ∧ (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉)) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) =
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) | 
| 119 | 15, 59, 76, 41, 118 | syl13anc 1374 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) =
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) | 
| 120 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) | 
| 121 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) | 
| 122 | 5, 32, 120, 121, 57 | drnginvrl 20756 | . . . . . . . . . . . . . 14
⊢
(((Scalar‘𝑊)
∈ DivRing ∧ 𝑘
∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠
(0g‘(Scalar‘𝑊))) →
(((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘) = (1r‘(Scalar‘𝑊))) | 
| 123 | 22, 23, 56, 122 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘) = (1r‘(Scalar‘𝑊))) | 
| 124 | 123 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠
‘𝑊)𝑌) =
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) | 
| 125 | 2, 4, 6, 5, 120 | lmodvsass 20885 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧
(((invr‘(Scalar‘𝑊))‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ 𝑉)) →
((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠
‘𝑊)𝑌) =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌))) | 
| 126 | 15, 59, 23, 74, 125 | syl13anc 1374 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠
‘𝑊)𝑌) =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌))) | 
| 127 | 2, 4, 6, 121 | lmodvs1 20888 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) | 
| 128 | 15, 74, 127 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) | 
| 129 | 124, 126,
128 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) = 𝑌) | 
| 130 | 129 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍))) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) | 
| 131 | 119, 130 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) | 
| 132 | 131 | sneqd 4638 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)))} = {(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}) | 
| 133 | 132 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍)))}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)(𝑙( ·𝑠 ‘𝑊)𝑍)))})) | 
| 134 | 117, 133 | eqtr3d 2779 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) | 
| 135 | 115, 134 | eleqtrd 2843 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) | 
| 136 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑌 + 𝑧) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) | 
| 137 | 136 | sneqd 4638 | . . . . . . . 8
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → {(𝑌 + 𝑧)} = {(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}) | 
| 138 | 137 | fveq2d 6910 | . . . . . . 7
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑁‘{(𝑌 + 𝑧)}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) | 
| 139 | 138 | eleq2d 2827 | . . . . . 6
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}) ↔ 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}))) | 
| 140 | 139 | rspcev 3622 | . . . . 5
⊢
(((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ∧ 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) | 
| 141 | 109, 135,
140 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) | 
| 142 | 141 | 3exp 1120 | . . 3
⊢ (𝜑 → ((𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) → (𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})))) | 
| 143 | 142 | rexlimdvv 3212 | . 2
⊢ (𝜑 → (∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))) | 
| 144 | 14, 143 | mpd 15 | 1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) |