Metamath Proof Explorer


Theorem lshpnel

Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpnel.v 𝑉 = ( Base ‘ 𝑊 )
lshpnel.n 𝑁 = ( LSpan ‘ 𝑊 )
lshpnel.p = ( LSSum ‘ 𝑊 )
lshpnel.h 𝐻 = ( LSHyp ‘ 𝑊 )
lshpnel.w ( 𝜑𝑊 ∈ LMod )
lshpnel.u ( 𝜑𝑈𝐻 )
lshpnel.x ( 𝜑𝑋𝑉 )
lshpnel.e ( 𝜑 → ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
Assertion lshpnel ( 𝜑 → ¬ 𝑋𝑈 )

Proof

Step Hyp Ref Expression
1 lshpnel.v 𝑉 = ( Base ‘ 𝑊 )
2 lshpnel.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lshpnel.p = ( LSSum ‘ 𝑊 )
4 lshpnel.h 𝐻 = ( LSHyp ‘ 𝑊 )
5 lshpnel.w ( 𝜑𝑊 ∈ LMod )
6 lshpnel.u ( 𝜑𝑈𝐻 )
7 lshpnel.x ( 𝜑𝑋𝑉 )
8 lshpnel.e ( 𝜑 → ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
9 1 4 5 6 lshpne ( 𝜑𝑈𝑉 )
10 5 adantr ( ( 𝜑𝑋𝑈 ) → 𝑊 ∈ LMod )
11 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
12 11 lsssssubg ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
13 10 12 syl ( ( 𝜑𝑋𝑈 ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
14 11 4 5 6 lshplss ( 𝜑𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
15 14 adantr ( ( 𝜑𝑋𝑈 ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
16 13 15 sseldd ( ( 𝜑𝑋𝑈 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
17 7 adantr ( ( 𝜑𝑋𝑈 ) → 𝑋𝑉 )
18 1 11 2 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19 10 17 18 syl2anc ( ( 𝜑𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
20 13 19 sseldd ( ( 𝜑𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
21 simpr ( ( 𝜑𝑋𝑈 ) → 𝑋𝑈 )
22 11 2 10 15 21 lspsnel5a ( ( 𝜑𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
23 3 lsmss2 ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) → ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑈 )
24 16 20 22 23 syl3anc ( ( 𝜑𝑋𝑈 ) → ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑈 )
25 8 adantr ( ( 𝜑𝑋𝑈 ) → ( 𝑈 ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
26 24 25 eqtr3d ( ( 𝜑𝑋𝑈 ) → 𝑈 = 𝑉 )
27 26 ex ( 𝜑 → ( 𝑋𝑈𝑈 = 𝑉 ) )
28 27 necon3ad ( 𝜑 → ( 𝑈𝑉 → ¬ 𝑋𝑈 ) )
29 9 28 mpd ( 𝜑 → ¬ 𝑋𝑈 )