Step | Hyp | Ref
| 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) |
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 20164 |
. . 3
⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑌, 𝑍}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)))) |
14 | 1, 13 | mpbid 235 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) |
15 | 10 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑊 ∈ LMod) |
16 | | eqid 2739 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
17 | 2, 16, 7 | lspsncl 20047 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) |
18 | 10, 12, 17 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) |
19 | 18 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) |
20 | 8 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑊 ∈ LVec) |
21 | 4 | lvecdrng 20175 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
DivRing) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (Scalar‘𝑊) ∈ DivRing) |
23 | | simp2l 1201 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
24 | | lspfixed.f |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍})) |
25 | 24 | 3ad2ant1 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‘𝑊))) |
28 | 27 | oveq1d 7250 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) |
29 | | simpl1 1193 |
. . . . . . . . . . . . . . . . 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 2739 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
33 | | lspfixed.o |
. . . . . . . . . . . . . . . . 17
⊢ 0 =
(0g‘𝑊) |
34 | 2, 4, 6, 32, 33 | lmod0vs 19965 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 0 ) |
35 | 30, 31, 34 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 0 ) |
36 | 28, 35 | eqtrd 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) = 0 ) |
37 | 36 | oveq1d 7250 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) = ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍))) |
38 | | simp2r 1202 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑙 ∈ (Base‘(Scalar‘𝑊))) |
39 | 12 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑍 ∈ 𝑉) |
40 | 2, 4, 6, 5 | lmodvscl 19949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑍 ∈ 𝑉) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) |
41 | 15, 38, 39, 40 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) |
43 | 2, 3, 33 | lmod0vlid 19962 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝑙(
·𝑠 ‘𝑊)𝑍) ∈ 𝑉) → ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍)) = (𝑙( ·𝑠
‘𝑊)𝑍)) |
44 | 30, 42, 43 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → ( 0 + (𝑙( ·𝑠
‘𝑊)𝑍)) = (𝑙( ·𝑠
‘𝑊)𝑍)) |
45 | 26, 37, 44 | 3eqtrd 2783 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑙( ·𝑠
‘𝑊)𝑍)) |
46 | 29, 18 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) |
47 | | simpl2r 1229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑙 ∈ (Base‘(Scalar‘𝑊))) |
48 | 2, 7 | lspsnid 20063 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → 𝑍 ∈ (𝑁‘{𝑍})) |
49 | 10, 12, 48 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ (𝑁‘{𝑍})) |
50 | 29, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑍 ∈ (𝑁‘{𝑍})) |
51 | 4, 6, 5, 16 | lssvscl 20025 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊)) ∧ (𝑙 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑍 ∈ (𝑁‘{𝑍}))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) |
52 | 30, 46, 47, 50, 51 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) |
53 | 45, 52 | eqeltrd 2840 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑘 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑍})) |
54 | 53 | ex 416 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑍}))) |
55 | 54 | necon3bd 2957 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑍}) → 𝑘 ≠
(0g‘(Scalar‘𝑊)))) |
56 | 25, 55 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑘 ≠
(0g‘(Scalar‘𝑊))) |
57 | | eqid 2739 |
. . . . . . . . 9
⊢
(invr‘(Scalar‘𝑊)) =
(invr‘(Scalar‘𝑊)) |
58 | 5, 32, 57 | drnginvrcl 19817 |
. . . . . . . 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 1135 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑍 ∈ (𝑁‘{𝑍})) |
61 | 15, 19, 38, 60, 51 | syl22anc 839 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙( ·𝑠
‘𝑊)𝑍) ∈ (𝑁‘{𝑍})) |
62 | 4, 6, 5, 16 | lssvscl 20025 |
. . . . . . 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 19818 |
. . . . . . . 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 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ¬ 𝑋 ∈ (𝑁‘{𝑌})) |
68 | | simpl3 1195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) |
69 | | oveq1 7242 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 =
(0g‘(Scalar‘𝑊)) → (𝑙( ·𝑠
‘𝑊)𝑍) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍)) |
70 | 2, 4, 6, 32, 33 | lmod0vs 19965 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍) = 0 ) |
71 | 15, 39, 70 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑍) = 0 ) |
72 | 69, 71 | sylan9eqr 2802 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑙( ·𝑠
‘𝑊)𝑍) = 0 ) |
73 | 72 | oveq2d 7251 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) = ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 )) |
74 | 11 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑌 ∈ 𝑉) |
75 | 2, 4, 6, 5 | lmodvscl 19949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
76 | 15, 23, 74, 75 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
77 | 2, 3, 33 | lmod0vrid 19963 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) |
78 | 15, 76, 77 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) |
79 | 78 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + 0 ) = (𝑘( ·𝑠
‘𝑊)𝑌)) |
80 | 68, 73, 79 | 3eqtrd 2783 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 = (𝑘( ·𝑠
‘𝑊)𝑌)) |
81 | 2, 16, 7 | lspsncl 20047 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
82 | 10, 11, 81 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
83 | 82 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) |
84 | 2, 7 | lspsnid 20063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ (𝑁‘{𝑌})) |
85 | 10, 11, 84 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑌})) |
86 | 85 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑌 ∈ (𝑁‘{𝑌})) |
87 | 4, 6, 5, 16 | lssvscl 20025 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ (𝑁‘{𝑌}))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) |
88 | 15, 83, 23, 86, 87 | syl22anc 839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) |
89 | 88 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘{𝑌})) |
90 | 80, 89 | eqeltrd 2840 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑙 = (0g‘(Scalar‘𝑊))) → 𝑋 ∈ (𝑁‘{𝑌})) |
91 | 90 | ex 416 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑙 = (0g‘(Scalar‘𝑊)) → 𝑋 ∈ (𝑁‘{𝑌}))) |
92 | 91 | necon3bd 2957 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (¬ 𝑋 ∈ (𝑁‘{𝑌}) → 𝑙 ≠
(0g‘(Scalar‘𝑊)))) |
93 | 67, 92 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑙 ≠
(0g‘(Scalar‘𝑊))) |
94 | | simpl1 1193 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝜑) |
95 | 94, 1 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
96 | | preq2 4667 |
. . . . . . . . . . . . . 14
⊢ (𝑍 = 0 → {𝑌, 𝑍} = {𝑌, 0 }) |
97 | 96 | fveq2d 6743 |
. . . . . . . . . . . . 13
⊢ (𝑍 = 0 → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌, 0 })) |
98 | 2, 33, 7, 15, 74 | lsppr0 20162 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{𝑌, 0 }) = (𝑁‘{𝑌})) |
99 | 97, 98 | sylan9eqr 2802 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌})) |
100 | 95, 99 | eleqtrd 2842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) ∧ 𝑍 = 0 ) → 𝑋 ∈ (𝑁‘{𝑌})) |
101 | 100 | ex 416 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑍 = 0 → 𝑋 ∈ (𝑁‘{𝑌}))) |
102 | 101 | necon3bd 2957 |
. . . . . . . . 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 20179 |
. . . . . . . 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 20179 |
. . . . . . 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 4717 |
. . . . . 6
⊢
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ↔
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ (𝑁‘{𝑍}) ∧
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ≠ 0 )) |
109 | 63, 107, 108 | sylanbrc 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 })) |
110 | | simp3 1140 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) |
111 | 2, 3 | lmodvacl 19946 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉 ∧ (𝑙( ·𝑠
‘𝑊)𝑍) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) |
112 | 15, 76, 41, 111 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) |
113 | 2, 7 | lspsnid 20063 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) |
114 | 15, 112, 113 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) |
115 | 110, 114 | eqeltrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))})) |
116 | 2, 4, 6, 5, 32, 7 | lspsnvs 20184 |
. . . . . . . 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 19955 |
. . . . . . . . . . 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 2739 |
. . . . . . . . . . . . . . 15
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
121 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
122 | 5, 32, 120, 121, 57 | drnginvrl 19819 |
. . . . . . . . . . . . . 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 7250 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)(.r‘(Scalar‘𝑊))𝑘)( ·𝑠
‘𝑊)𝑌) =
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) |
125 | 2, 4, 6, 5, 120 | lmodvsass 19957 |
. . . . . . . . . . . . 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 19960 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) |
128 | 15, 74, 127 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) |
129 | 124, 126,
128 | 3eqtr3d 2787 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) = 𝑌) |
130 | 129 | oveq1d 7250 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑘(
·𝑠 ‘𝑊)𝑌)) +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍))) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) |
131 | 119, 130 | eqtrd 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) |
132 | 131 | sneqd 4570 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) →
{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)((𝑘(
·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)))} = {(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}) |
133 | 132 | fveq2d 6743 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)((𝑘( ·𝑠 ‘𝑊)𝑌) + (𝑙( ·𝑠 ‘𝑊)𝑍)))}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠 ‘𝑊)(𝑙( ·𝑠 ‘𝑊)𝑍)))})) |
134 | 117, 133 | eqtr3d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → (𝑁‘{((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) |
135 | 115, 134 | eleqtrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) |
136 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑌 + 𝑧) = (𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))) |
137 | 136 | sneqd 4570 |
. . . . . . . 8
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → {(𝑌 + 𝑧)} = {(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}) |
138 | 137 | fveq2d 6743 |
. . . . . . 7
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑁‘{(𝑌 + 𝑧)}) = (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) |
139 | 138 | eleq2d 2825 |
. . . . . 6
⊢ (𝑧 =
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) → (𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}) ↔ 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))}))) |
140 | 139 | rspcev 3552 |
. . . . 5
⊢
(((((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)) ∈ ((𝑁‘{𝑍}) ∖ { 0 }) ∧ 𝑋 ∈ (𝑁‘{(𝑌 +
(((invr‘(Scalar‘𝑊))‘𝑘)( ·𝑠
‘𝑊)(𝑙(
·𝑠 ‘𝑊)𝑍)))})) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) |
141 | 109, 135,
140 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍))) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) |
142 | 141 | 3exp 1121 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑙 ∈ (Base‘(Scalar‘𝑊))) → (𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})))) |
143 | 142 | rexlimdvv 3222 |
. 2
⊢ (𝜑 → (∃𝑘 ∈ (Base‘(Scalar‘𝑊))∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑋 = ((𝑘( ·𝑠
‘𝑊)𝑌) + (𝑙( ·𝑠
‘𝑊)𝑍)) → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)}))) |
144 | 14, 143 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ((𝑁‘{𝑍}) ∖ { 0 })𝑋 ∈ (𝑁‘{(𝑌 + 𝑧)})) |