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	ellspsn5	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
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	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )

Metamath Proof Explorer

Theorem lshpnel

Proof