Theorem dvh3dim

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

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

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		dvh3dim.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8	1 2 3 4 5 7	dvh2dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 } ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 } ) )
10		prcom	⊢ { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
11		preq2	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑌 , 𝑋 } = { 𝑌 , ( 0g ‘ 𝑈 ) } )
12	10 11	syl5eq	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 } = { 𝑌 , ( 0g ‘ 𝑈 ) } )
13	12	fveq2d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , ( 0g ‘ 𝑈 ) } ) )
14		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15	1 2 5	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
16	3 14 4 15 7	lsppr0	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , ( 0g ‘ 𝑈 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
17	13 16	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 } ) )
18	17	eleq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
19	18	notbid	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
20	19	rexbidv	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
21	9 20	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
22	1 2 3 4 5 6	dvh2dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
24		preq2	⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 } = { 𝑋 , ( 0g ‘ 𝑈 ) } )
25	24	fveq2d	⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 , ( 0g ‘ 𝑈 ) } ) )
26	3 14 4 15 6	lsppr0	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 0g ‘ 𝑈 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
27	25 26	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )
28	27	eleq2d	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) )
29	28	notbid	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) )
30	29	rexbidv	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) )
31	23 30	mpbird	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
32	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
34	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
35		simprl	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
36		simprr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ≠ ( 0g ‘ 𝑈 ) )
37	1 2 3 4 32 33 34 14 35 36	dvhdimlem	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
38	21 31 37	pm2.61da2ne	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )