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