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