Step | Hyp | Ref
| Expression |
1 | | lshpdisj.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 20143 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | 3 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝑊 ∈ LMod) |
5 | | lshpdisj.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
6 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝑋 ∈ 𝑉) |
7 | | eqid 2737 |
. . . . . . . 8
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
8 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
9 | | lshpdisj.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
10 | | eqid 2737 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
11 | | lshpdisj.n |
. . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑊) |
12 | 7, 8, 9, 10, 11 | lspsnel 20040 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑣 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) |
13 | 4, 6, 12 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ (𝑁‘{𝑋}) ↔ ∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋))) |
14 | | lshpdisj.p |
. . . . . . . . . . . . . . . . 17
⊢ ⊕ =
(LSSum‘𝑊) |
15 | | lshpdisj.h |
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = (LSHyp‘𝑊) |
16 | | lshpdisj.u |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ 𝐻) |
17 | | lshpdisj.e |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) |
18 | 9, 11, 14, 15, 3, 16, 5, 17 | lshpnel 36734 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) |
19 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → ¬ 𝑋 ∈ 𝑈) |
20 | | lshpdisj.o |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑊) |
21 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
22 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → 𝑊 ∈ LVec) |
23 | 21, 15, 3, 16 | lshplss 36732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊)) |
24 | 23 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → 𝑈 ∈ (LSubSp‘𝑊)) |
25 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → 𝑋 ∈ 𝑉) |
26 | 3 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod) |
27 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑘 ∈ (Base‘(Scalar‘𝑊))) |
28 | 5 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑋 ∈ 𝑉) |
29 | 9, 10, 7, 8, 11, 26, 27, 28 | lspsneli 20038 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·𝑠
‘𝑊)𝑋) ∈ (𝑁‘{𝑋})) |
30 | 29 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → (𝑘(
·𝑠 ‘𝑊)𝑋) ∈ (𝑁‘{𝑋})) |
31 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → (𝑘(
·𝑠 ‘𝑊)𝑋) ≠ 0 ) |
32 | 9, 20, 21, 11, 22, 24, 25, 30, 31 | lspsnel4 20161 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → (𝑋 ∈ 𝑈 ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ 𝑈)) |
33 | 19, 32 | mtbid 327 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 ) → ¬ (𝑘(
·𝑠 ‘𝑊)𝑋) ∈ 𝑈) |
34 | 33 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ≠ 0 → ¬ (𝑘(
·𝑠 ‘𝑊)𝑋) ∈ 𝑈)) |
35 | 34 | necon4ad 2959 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·𝑠
‘𝑊)𝑋) ∈ 𝑈 → (𝑘( ·𝑠
‘𝑊)𝑋) = 0 )) |
36 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → (𝑣 ∈ 𝑈 ↔ (𝑘( ·𝑠
‘𝑊)𝑋) ∈ 𝑈)) |
37 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → (𝑣 = 0 ↔ (𝑘( ·𝑠
‘𝑊)𝑋) = 0 )) |
38 | 36, 37 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → ((𝑣 ∈ 𝑈 → 𝑣 = 0 ) ↔ ((𝑘(
·𝑠 ‘𝑊)𝑋) ∈ 𝑈 → (𝑘( ·𝑠
‘𝑊)𝑋) = 0 ))) |
39 | 35, 38 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → (𝑣 ∈ 𝑈 → 𝑣 = 0 ))) |
40 | 39 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → (𝑣 ∈ 𝑈 → 𝑣 = 0 )))) |
41 | 40 | com23 86 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 ∈ 𝑈 → 𝑣 = 0 )))) |
42 | 41 | com24 95 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ 𝑈 → (𝑘 ∈ (Base‘(Scalar‘𝑊)) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 )))) |
43 | 42 | imp31 421 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 )) |
44 | 43 | rexlimdva 3203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (∃𝑘 ∈ (Base‘(Scalar‘𝑊))𝑣 = (𝑘( ·𝑠
‘𝑊)𝑋) → 𝑣 = 0 )) |
45 | 13, 44 | sylbid 243 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ (𝑁‘{𝑋}) → 𝑣 = 0 )) |
46 | 45 | expimpd 457 |
. . . 4
⊢ (𝜑 → ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ (𝑁‘{𝑋})) → 𝑣 = 0 )) |
47 | | elin 3882 |
. . . 4
⊢ (𝑣 ∈ (𝑈 ∩ (𝑁‘{𝑋})) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ (𝑁‘{𝑋}))) |
48 | | velsn 4557 |
. . . 4
⊢ (𝑣 ∈ { 0 } ↔ 𝑣 = 0 ) |
49 | 46, 47, 48 | 3imtr4g 299 |
. . 3
⊢ (𝜑 → (𝑣 ∈ (𝑈 ∩ (𝑁‘{𝑋})) → 𝑣 ∈ { 0 })) |
50 | 49 | ssrdv 3907 |
. 2
⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) ⊆ { 0 }) |
51 | 9, 21, 11 | lspsncl 20014 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
52 | 3, 5, 51 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
53 | 21 | lssincl 20002 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) → (𝑈 ∩ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) |
54 | 3, 23, 52, 53 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) |
55 | 20, 21 | lss0ss 19985 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ∩ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) → { 0 } ⊆ (𝑈 ∩ (𝑁‘{𝑋}))) |
56 | 3, 54, 55 | syl2anc 587 |
. 2
⊢ (𝜑 → { 0 } ⊆ (𝑈 ∩ (𝑁‘{𝑋}))) |
57 | 50, 56 | eqssd 3918 |
1
⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑋})) = { 0 }) |