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