This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑋 = ( 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 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )