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

Metamath Proof Explorer

Theorem dvhdimlem

Proof