Step | Hyp | Ref
| Expression |
1 | | lspsolv.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
2 | | lspsolv.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
3 | | lspsolv.n |
. . 3
⊢ 𝑁 = (LSpan‘𝑊) |
4 | | eqid 2738 |
. . 3
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
5 | | eqid 2738 |
. . 3
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
6 | | eqid 2738 |
. . 3
⊢
(+g‘𝑊) = (+g‘𝑊) |
7 | | eqid 2738 |
. . 3
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
8 | | eqid 2738 |
. . 3
⊢ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ (Base‘(Scalar‘𝑊))(𝑧(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴)} = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ (Base‘(Scalar‘𝑊))(𝑧(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴)} |
9 | | lveclmod 20368 |
. . . 4
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
10 | 9 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑊 ∈ LMod) |
11 | | simpr1 1193 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝐴 ⊆ 𝑉) |
12 | | simpr2 1194 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑌 ∈ 𝑉) |
13 | | simpr3 1195 |
. . . 4
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴))) |
14 | 13 | eldifad 3899 |
. . 3
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌}))) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 14 | lspsolvlem 20404 |
. 2
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → ∃𝑟 ∈ (Base‘(Scalar‘𝑊))(𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴)) |
16 | 4 | lvecdrng 20367 |
. . . . . . 7
⊢ (𝑊 ∈ LVec →
(Scalar‘𝑊) ∈
DivRing) |
17 | 16 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (Scalar‘𝑊) ∈ DivRing) |
18 | | simprl 768 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
19 | 10 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑊 ∈ LMod) |
20 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑌 ∈ 𝑉) |
21 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
22 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑊) = (0g‘𝑊) |
23 | 1, 4, 7, 21, 22 | lmod0vs 20156 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = (0g‘𝑊)) |
24 | 19, 20, 23 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = (0g‘𝑊)) |
25 | 24 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) = (𝑋(+g‘𝑊)(0g‘𝑊))) |
26 | 11 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝐴 ⊆ 𝑉) |
27 | 20 | snssd 4742 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → {𝑌} ⊆ 𝑉) |
28 | 26, 27 | unssd 4120 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝐴 ∪ {𝑌}) ⊆ 𝑉) |
29 | 1, 3 | lspssv 20245 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ {𝑌}) ⊆ 𝑉) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑉) |
30 | 19, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑉) |
31 | 30 | ssdifssd 4077 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)) ⊆ 𝑉) |
32 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴))) |
33 | 31, 32 | sseldd 3922 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑋 ∈ 𝑉) |
34 | 1, 6, 22 | lmod0vrid 20154 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋(+g‘𝑊)(0g‘𝑊)) = 𝑋) |
35 | 19, 33, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)(0g‘𝑊)) = 𝑋) |
36 | 25, 35 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) = 𝑋) |
37 | 36, 32 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴))) |
38 | 37 | eldifbd 3900 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → ¬ (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘𝐴)) |
39 | | simprr 770 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴)) |
40 | | oveq1 7282 |
. . . . . . . . . . 11
⊢ (𝑟 =
(0g‘(Scalar‘𝑊)) → (𝑟( ·𝑠
‘𝑊)𝑌) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) |
41 | 40 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑟 =
(0g‘(Scalar‘𝑊)) → (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) = (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌))) |
42 | 41 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑟 =
(0g‘(Scalar‘𝑊)) → ((𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) |
43 | 39, 42 | syl5ibcom 244 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑟 = (0g‘(Scalar‘𝑊)) → (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) |
44 | 43 | necon3bd 2957 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (¬ (𝑋(+g‘𝑊)((0g‘(Scalar‘𝑊))(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘𝐴) → 𝑟 ≠
(0g‘(Scalar‘𝑊)))) |
45 | 38, 44 | mpd 15 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑟 ≠
(0g‘(Scalar‘𝑊))) |
46 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
47 | | eqid 2738 |
. . . . . . 7
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
48 | | eqid 2738 |
. . . . . . 7
⊢
(invr‘(Scalar‘𝑊)) =
(invr‘(Scalar‘𝑊)) |
49 | 5, 21, 46, 47, 48 | drnginvrl 20010 |
. . . . . 6
⊢
(((Scalar‘𝑊)
∈ DivRing ∧ 𝑟
∈ (Base‘(Scalar‘𝑊)) ∧ 𝑟 ≠
(0g‘(Scalar‘𝑊))) →
(((invr‘(Scalar‘𝑊))‘𝑟)(.r‘(Scalar‘𝑊))𝑟) = (1r‘(Scalar‘𝑊))) |
50 | 17, 18, 45, 49 | syl3anc 1370 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
(((invr‘(Scalar‘𝑊))‘𝑟)(.r‘(Scalar‘𝑊))𝑟) = (1r‘(Scalar‘𝑊))) |
51 | 50 | oveq1d 7290 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
((((invr‘(Scalar‘𝑊))‘𝑟)(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑌) =
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌)) |
52 | 5, 21, 48 | drnginvrcl 20008 |
. . . . . 6
⊢
(((Scalar‘𝑊)
∈ DivRing ∧ 𝑟
∈ (Base‘(Scalar‘𝑊)) ∧ 𝑟 ≠
(0g‘(Scalar‘𝑊))) →
((invr‘(Scalar‘𝑊))‘𝑟) ∈ (Base‘(Scalar‘𝑊))) |
53 | 17, 18, 45, 52 | syl3anc 1370 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
((invr‘(Scalar‘𝑊))‘𝑟) ∈ (Base‘(Scalar‘𝑊))) |
54 | 1, 4, 7, 5, 46 | lmodvsass 20148 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧
(((invr‘(Scalar‘𝑊))‘𝑟) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ 𝑉)) →
((((invr‘(Scalar‘𝑊))‘𝑟)(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑌) =
(((invr‘(Scalar‘𝑊))‘𝑟)( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑌))) |
55 | 19, 53, 18, 20, 54 | syl13anc 1371 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
((((invr‘(Scalar‘𝑊))‘𝑟)(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑌) =
(((invr‘(Scalar‘𝑊))‘𝑟)( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑌))) |
56 | 1, 4, 7, 47 | lmodvs1 20151 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) |
57 | 19, 20, 56 | syl2anc 584 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑌) = 𝑌) |
58 | 51, 55, 57 | 3eqtr3d 2786 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
(((invr‘(Scalar‘𝑊))‘𝑟)( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑌)) = 𝑌) |
59 | 33 | snssd 4742 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → {𝑋} ⊆ 𝑉) |
60 | 26, 59 | unssd 4120 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝐴 ∪ {𝑋}) ⊆ 𝑉) |
61 | 1, 2, 3 | lspcl 20238 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ {𝑋}) ⊆ 𝑉) → (𝑁‘(𝐴 ∪ {𝑋})) ∈ 𝑆) |
62 | 19, 60, 61 | syl2anc 584 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘(𝐴 ∪ {𝑋})) ∈ 𝑆) |
63 | 1, 4, 7, 5 | lmodvscl 20140 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
64 | 19, 18, 20, 63 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑟( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
65 | | eqid 2738 |
. . . . . . 7
⊢
(-g‘𝑊) = (-g‘𝑊) |
66 | 1, 6, 65 | lmodvpncan 20176 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋)(-g‘𝑊)𝑋) = (𝑟( ·𝑠
‘𝑊)𝑌)) |
67 | 19, 64, 33, 66 | syl3anc 1370 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋)(-g‘𝑊)𝑋) = (𝑟( ·𝑠
‘𝑊)𝑌)) |
68 | 1, 6 | lmodcom 20169 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑌) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋) = (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌))) |
69 | 19, 64, 33, 68 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → ((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋) = (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌))) |
70 | | ssun1 4106 |
. . . . . . . . . 10
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑋}) |
71 | 70 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝐴 ⊆ (𝐴 ∪ {𝑋})) |
72 | 1, 3 | lspss 20246 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ {𝑋}) ⊆ 𝑉 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑋})) → (𝑁‘𝐴) ⊆ (𝑁‘(𝐴 ∪ {𝑋}))) |
73 | 19, 60, 71, 72 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘𝐴) ⊆ (𝑁‘(𝐴 ∪ {𝑋}))) |
74 | 73, 39 | sseldd 3922 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
75 | 69, 74 | eqeltrd 2839 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → ((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
76 | 1, 3 | lspssid 20247 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ {𝑋}) ⊆ 𝑉) → (𝐴 ∪ {𝑋}) ⊆ (𝑁‘(𝐴 ∪ {𝑋}))) |
77 | 19, 60, 76 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝐴 ∪ {𝑋}) ⊆ (𝑁‘(𝐴 ∪ {𝑋}))) |
78 | | snidg 4595 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
79 | | elun2 4111 |
. . . . . . . 8
⊢ (𝑋 ∈ {𝑋} → 𝑋 ∈ (𝐴 ∪ {𝑋})) |
80 | 33, 78, 79 | 3syl 18 |
. . . . . . 7
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑋 ∈ (𝐴 ∪ {𝑋})) |
81 | 77, 80 | sseldd 3922 |
. . . . . 6
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
82 | 65, 2 | lssvsubcl 20205 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘(𝐴 ∪ {𝑋})) ∈ 𝑆) ∧ (((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ (𝑁‘(𝐴 ∪ {𝑋})) ∧ 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑋})))) → (((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋)(-g‘𝑊)𝑋) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
83 | 19, 62, 75, 81, 82 | syl22anc 836 |
. . . . 5
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (((𝑟( ·𝑠
‘𝑊)𝑌)(+g‘𝑊)𝑋)(-g‘𝑊)𝑋) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
84 | 67, 83 | eqeltrrd 2840 |
. . . 4
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → (𝑟( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
85 | 4, 7, 5, 2 | lssvscl 20217 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ (𝑁‘(𝐴 ∪ {𝑋})) ∈ 𝑆) ∧
(((invr‘(Scalar‘𝑊))‘𝑟) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑟( ·𝑠
‘𝑊)𝑌) ∈ (𝑁‘(𝐴 ∪ {𝑋})))) →
(((invr‘(Scalar‘𝑊))‘𝑟)( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
86 | 19, 62, 53, 84, 85 | syl22anc 836 |
. . 3
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) →
(((invr‘(Scalar‘𝑊))‘𝑟)( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑌)) ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
87 | 58, 86 | eqeltrrd 2840 |
. 2
⊢ (((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑋(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑌)) ∈ (𝑁‘𝐴))) → 𝑌 ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |
88 | 15, 87 | rexlimddv 3220 |
1
⊢ ((𝑊 ∈ LVec ∧ (𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ((𝑁‘(𝐴 ∪ {𝑌})) ∖ (𝑁‘𝐴)))) → 𝑌 ∈ (𝑁‘(𝐴 ∪ {𝑋}))) |