Step | Hyp | Ref
| Expression |
1 | | lspdisj.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 20368 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lspdisj.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
5 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
6 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
7 | | lspdisj.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
8 | | eqid 2738 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
9 | | lspdisj.n |
. . . . . . . . . 10
⊢ 𝑁 = (LSpan‘𝑊) |
10 | 5, 6, 7, 8, 9 | lspsnel 20265 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑣 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) |
11 | 3, 4, 10 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) |
12 | 11 | biimpa 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑁‘{𝑋})) → ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋)) |
13 | 12 | adantrr 714 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈)) → ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋)) |
14 | | simprr 770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋)) |
15 | | lspdisj.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) |
16 | 15 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → ¬ 𝑋 ∈ 𝑈) |
17 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑣 ∈ 𝑈) |
18 | 14, 17 | eqeltrrd 2840 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ 𝑈) |
19 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
20 | | lspdisj.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = (LSubSp‘𝑊) |
21 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑊 ∈ LVec) |
22 | | lspdisj.u |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
23 | 22 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑈 ∈ 𝑆) |
24 | 4 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑋 ∈ 𝑉) |
25 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
26 | 7, 8, 5, 6, 19, 20, 21, 23, 24, 25 | lssvs0or 20372 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ 𝑈 ↔ (𝑘 = (0g‘(Scalar‘𝑊)) ∨ 𝑋 ∈ 𝑈))) |
27 | 18, 26 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → (𝑘 = (0g‘(Scalar‘𝑊)) ∨ 𝑋 ∈ 𝑈)) |
28 | 27 | orcomd 868 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → (𝑋 ∈ 𝑈 ∨ 𝑘 = (0g‘(Scalar‘𝑊)))) |
29 | 28 | ord 861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → (¬ 𝑋 ∈ 𝑈 → 𝑘 = (0g‘(Scalar‘𝑊)))) |
30 | 16, 29 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑘 = (0g‘(Scalar‘𝑊))) |
31 | 30 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → (𝑘( ·𝑠
‘𝑊)𝑋) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑋)) |
32 | 3 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑊 ∈ LMod) |
33 | | lspdisj.o |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑊) |
34 | 7, 5, 8, 19, 33 | lmod0vs 20156 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑋) = 0 ) |
35 | 32, 24, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑋) = 0 ) |
36 | 14, 31, 35 | 3eqtrd 2782 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) → 𝑣 = 0 ) |
37 | 36 | exp32 421 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 ))) |
38 | 37 | adantrl 713 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈)) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 ))) |
39 | 38 | rexlimdv 3212 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈)) → (∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 )) |
40 | 13, 39 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈)) → 𝑣 = 0 ) |
41 | 40 | ex 413 |
. . . 4
⊢ (𝜑 → ((𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈) → 𝑣 = 0 )) |
42 | | elin 3903 |
. . . 4
⊢ (𝑣 ∈ ((𝑁‘{𝑋}) ∩ 𝑈) ↔ (𝑣 ∈ (𝑁‘{𝑋}) ∧ 𝑣 ∈ 𝑈)) |
43 | | velsn 4577 |
. . . 4
⊢ (𝑣 ∈ { 0 } ↔ 𝑣 = 0 ) |
44 | 41, 42, 43 | 3imtr4g 296 |
. . 3
⊢ (𝜑 → (𝑣 ∈ ((𝑁‘{𝑋}) ∩ 𝑈) → 𝑣 ∈ { 0 })) |
45 | 44 | ssrdv 3927 |
. 2
⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ 𝑈) ⊆ { 0 }) |
46 | 7, 20, 9 | lspsncl 20239 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ 𝑆) |
47 | 3, 4, 46 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝑆) |
48 | 33, 20 | lss0ss 20210 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑋}) ∈ 𝑆) → { 0 } ⊆ (𝑁‘{𝑋})) |
49 | 3, 47, 48 | syl2anc 584 |
. . 3
⊢ (𝜑 → { 0 } ⊆ (𝑁‘{𝑋})) |
50 | 33, 20 | lss0ss 20210 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → { 0 } ⊆ 𝑈) |
51 | 3, 22, 50 | syl2anc 584 |
. . 3
⊢ (𝜑 → { 0 } ⊆ 𝑈) |
52 | 49, 51 | ssind 4166 |
. 2
⊢ (𝜑 → { 0 } ⊆ ((𝑁‘{𝑋}) ∩ 𝑈)) |
53 | 45, 52 | eqssd 3938 |
1
⊢ (𝜑 → ((𝑁‘{𝑋}) ∩ 𝑈) = { 0 }) |