This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lshpnel2N

Description: Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lshpnel2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpnel2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lshpnel2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpnel2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpnel2.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpnel2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpnel2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lshpnel2.t ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
lshpnel2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lshpnel2.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
Assertion lshpnel2N ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lshpnel2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpnel2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lshpnel2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpnel2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lshpnel2.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpnel2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lshpnel2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8 lshpnel2.t ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
9 lshpnel2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lshpnel2.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → ¬ 𝑋 ∈ 𝑈 )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → 𝑊 ∈ LVec )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → 𝑈 ∈ 𝐻 )
14 9 adantr ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → 𝑋 ∈ 𝑉 )
15 1 3 4 5 12 13 14 lshpnelb ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → ( ¬ 𝑋 ∈ 𝑈 ↔ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )
16 11 15 mpbid ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐻 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
17 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑈 ∈ 𝑆 )
18 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑈 ≠ 𝑉 )
19 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑋 ∈ 𝑉 )
20 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
21 6 20 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
22 2 3 lspid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
23 21 7 22 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) = 𝑈 )
24 23 uneq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑈 ∪ ( 𝑁 ‘ { 𝑋 } ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
26 1 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
27 7 26 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
28 9 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
29 1 3 lspun ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
30 21 27 28 29 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ 𝑈 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
31 1 2 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
32 21 9 31 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
33 2 3 4 lsmsp ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
34 21 7 32 33 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
35 25 30 34 3eqtr4rd ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) )
36 35 eqeq1d ⊢ ( 𝜑 → ( ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ↔ ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = 𝑉 ) )
37 36 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = 𝑉 )
38 sneq ⊢ ( 𝑣 = 𝑋 → { 𝑣 } = { 𝑋 } )
39 38 uneq2d ⊢ ( 𝑣 = 𝑋 → ( 𝑈 ∪ { 𝑣 } ) = ( 𝑈 ∪ { 𝑋 } ) )
40 39 fveqeq2d ⊢ ( 𝑣 = 𝑋 → ( ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ↔ ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = 𝑉 ) )
41 40 rspcev ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ ( 𝑈 ∪ { 𝑋 } ) ) = 𝑉 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 )
42 19 37 41 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 )
43 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑊 ∈ LVec )
44 1 3 2 5 islshp ⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
45 43 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
46 17 18 42 45 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) → 𝑈 ∈ 𝐻 )
47 16 46 impbida ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )