Theorem dvh2dim

Description: There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dvh3dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvh3dim.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvh3dim.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dvh3dim.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dvh3dim.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dvh3dim.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	dvh2dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvh3dim.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dvh3dim.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		dvh3dim.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5		dvh3dim.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		dvh3dim.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
8	1 2 3 7 5	dvh1dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ ( 0g ‘ 𝑈 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 𝑧 ≠ ( 0g ‘ 𝑈 ) )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → 𝑋 = ( 0g ‘ 𝑈 ) )
11	10	sneqd	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → { 𝑋 } = { ( 0g ‘ 𝑈 ) } )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
13	1 2 5	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14	7 4	lspsn0	⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
15	13 14	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
17	12 16	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 } ) = { ( 0g ‘ 𝑈 ) } )
18	17	eleq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑧 ∈ { ( 0g ‘ 𝑈 ) } ) )
19		velsn	⊢ ( 𝑧 ∈ { ( 0g ‘ 𝑈 ) } ↔ 𝑧 = ( 0g ‘ 𝑈 ) )
20	18 19	bitrdi	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑧 = ( 0g ‘ 𝑈 ) ) )
21	20	necon3bbid	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) )
22	21	rexbidv	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑧 ∈ 𝑉 𝑧 ≠ ( 0g ‘ 𝑈 ) ) )
23	9 22	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
24	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ 𝑉 )
26		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
27	1 2 3 4 24 25 25 7 26 26	dvhdimlem	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑋 } ) )
28		dfsn2	⊢ { 𝑋 } = { 𝑋 , 𝑋 }
29	28	fveq2i	⊢ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 , 𝑋 } )
30	29	eleq2i	⊢ ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑋 } ) )
31	30	notbii	⊢ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑋 } ) )
32	31	rexbii	⊢ ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑋 } ) )
33	27 32	sylibr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
34	23 33	pm2.61dane	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )