Metamath Proof Explorer


Theorem dvhdimlem

Description: Lemma for dvh2dim and dvh3dim . TODO: make this obsolete and use dvh4dimlem directly? (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 ( 𝜑𝑋𝑉 )
dvhdim.y ( 𝜑𝑌𝑉 )
dvhdim.o 0 = ( 0g𝑈 )
dvhdim.x ( 𝜑𝑋0 )
dvhdimlem.y ( 𝜑𝑌0 )
Assertion dvhdimlem ( 𝜑 → ∃ 𝑧𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

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 dvhdim.y ( 𝜑𝑌𝑉 )
8 dvhdim.o 0 = ( 0g𝑈 )
9 dvhdim.x ( 𝜑𝑋0 )
10 dvhdimlem.y ( 𝜑𝑌0 )
11 1 2 3 4 5 6 7 7 8 9 10 10 dvh4dimlem ( 𝜑 → ∃ 𝑧𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑌 } ) )
12 1 2 5 dvhlmod ( 𝜑𝑈 ∈ LMod )
13 df-tp { 𝑋 , 𝑌 , 𝑌 } = ( { 𝑋 , 𝑌 } ∪ { 𝑌 } )
14 prssi ( ( 𝑋𝑉𝑌𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
15 6 7 14 syl2anc ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
16 7 snssd ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
17 15 16 unssd ( 𝜑 → ( { 𝑋 , 𝑌 } ∪ { 𝑌 } ) ⊆ 𝑉 )
18 13 17 eqsstrid ( 𝜑 → { 𝑋 , 𝑌 , 𝑌 } ⊆ 𝑉 )
19 ssun1 { 𝑋 , 𝑌 } ⊆ ( { 𝑋 , 𝑌 } ∪ { 𝑌 } )
20 19 13 sseqtrri { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 , 𝑌 }
21 20 a1i ( 𝜑 → { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 , 𝑌 } )
22 3 4 lspss ( ( 𝑈 ∈ LMod ∧ { 𝑋 , 𝑌 , 𝑌 } ⊆ 𝑉 ∧ { 𝑋 , 𝑌 } ⊆ { 𝑋 , 𝑌 , 𝑌 } ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑌 } ) )
23 12 18 21 22 syl3anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑌 } ) )
24 23 ssneld ( 𝜑 → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑌 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
25 24 reximdv ( 𝜑 → ( ∃ 𝑧𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑌 } ) → ∃ 𝑧𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
26 11 25 mpd ( 𝜑 → ∃ 𝑧𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )