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 ( 𝜑 → ( 𝑈𝐻 ↔ ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )