Metamath Proof Explorer

Theorem lshpdisj

Description: A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpdisj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpdisj.o ⊢ 0 = ( 0g ‘ 𝑊 )
lshpdisj.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpdisj.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpdisj.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpdisj.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpdisj.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpdisj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lshpdisj.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
Assertion lshpdisj ( 𝜑 → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑋 } ) ) = { 0 } )

Proof

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