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

Metamath Proof Explorer

Theorem dvh4dimN

Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015) (New usage is discouraged.)

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

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 dvh3dim2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 1 2 3 4 5 7 8 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
11 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 prssi ⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → { 𝑌 , 𝑍 } ⊆ 𝑉 )
14 7 8 13 syl2anc ⊢ ( 𝜑 → { 𝑌 , 𝑍 } ⊆ 𝑉 )
15 3 11 4 12 14 lspun0 ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
16 tprot ⊢ { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 } = { 𝑌 , 𝑍 , ( 0g ‘ 𝑈 ) }
17 df-tp ⊢ { 𝑌 , 𝑍 , ( 0g ‘ 𝑈 ) } = ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } )
18 16 17 eqtr2i ⊢ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 }
19 tpeq1 ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 } )
20 18 19 eqtr4id ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
21 20 fveq2d ⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
22 15 21 sylan9req ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
23 22 eleq2d ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
24 23 notbid ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
25 24 rexbidv ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
26 10 25 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
27 1 2 3 4 5 6 8 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
29 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → { 𝑋 , 𝑍 } ⊆ 𝑉 )
30 6 8 29 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑍 } ⊆ 𝑉 )
31 3 11 4 12 30 lspun0 ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
32 df-tp ⊢ { 𝑋 , 𝑍 , ( 0g ‘ 𝑈 ) } = ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } )
33 tpcomb ⊢ { 𝑋 , 𝑍 , ( 0g ‘ 𝑈 ) } = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 }
34 32 33 eqtr3i ⊢ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 }
35 tpeq2 ⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 } )
36 34 35 eqtr4id ⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
37 36 fveq2d ⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
38 31 37 sylan9req ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
39 38 eleq2d ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
40 39 notbid ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
41 40 rexbidv ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
42 28 41 mpbid ⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
43 1 2 3 4 5 6 7 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
45 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
46 6 7 45 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
47 3 11 4 12 46 lspun0 ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
48 tpeq3 ⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { 𝑋 , 𝑌 , ( 0g ‘ 𝑈 ) } )
49 df-tp ⊢ { 𝑋 , 𝑌 , ( 0g ‘ 𝑈 ) } = ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } )
50 48 49 eqtr2di ⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
51 50 fveq2d ⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
52 47 51 sylan9req ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
53 52 eleq2d ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
54 53 notbid ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
55 54 rexbidv ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
56 44 55 mpbid ⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
57 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
58 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
59 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
60 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑍 ∈ 𝑉 )
61 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
62 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ≠ ( 0g ‘ 𝑈 ) )
63 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑍 ≠ ( 0g ‘ 𝑈 ) )
64 1 2 3 4 57 58 59 60 11 61 62 63 dvh4dimlem ⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
65 26 42 56 64 pm2.61da3ne ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )