# 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 ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dvh3dim.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dvh3dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dvh3dim.x ${⊢}{\phi }\to {X}\in {V}$
dvhdim.y ${⊢}{\phi }\to {Y}\in {V}$
dvhdim.o
dvhdim.x
dvhdimlem.y
Assertion dvhdimlem ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 dvh3dim.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dvh3dim.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dvh3dim.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dvh3dim.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
5 dvh3dim.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 dvh3dim.x ${⊢}{\phi }\to {X}\in {V}$
7 dvhdim.y ${⊢}{\phi }\to {Y}\in {V}$
8 dvhdim.o
9 dvhdim.x
10 dvhdimlem.y
11 1 2 3 4 5 6 7 7 8 9 10 10 dvh4dimlem ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Y}\right\}\right)$
12 1 2 5 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
13 df-tp ${⊢}\left\{{X},{Y},{Y}\right\}=\left\{{X},{Y}\right\}\cup \left\{{Y}\right\}$
14 prssi ${⊢}\left({X}\in {V}\wedge {Y}\in {V}\right)\to \left\{{X},{Y}\right\}\subseteq {V}$
15 6 7 14 syl2anc ${⊢}{\phi }\to \left\{{X},{Y}\right\}\subseteq {V}$
16 7 snssd ${⊢}{\phi }\to \left\{{Y}\right\}\subseteq {V}$
17 15 16 unssd ${⊢}{\phi }\to \left\{{X},{Y}\right\}\cup \left\{{Y}\right\}\subseteq {V}$
18 13 17 eqsstrid ${⊢}{\phi }\to \left\{{X},{Y},{Y}\right\}\subseteq {V}$
19 ssun1 ${⊢}\left\{{X},{Y}\right\}\subseteq \left\{{X},{Y}\right\}\cup \left\{{Y}\right\}$
20 19 13 sseqtrri ${⊢}\left\{{X},{Y}\right\}\subseteq \left\{{X},{Y},{Y}\right\}$
21 20 a1i ${⊢}{\phi }\to \left\{{X},{Y}\right\}\subseteq \left\{{X},{Y},{Y}\right\}$
22 3 4 lspss ${⊢}\left({U}\in \mathrm{LMod}\wedge \left\{{X},{Y},{Y}\right\}\subseteq {V}\wedge \left\{{X},{Y}\right\}\subseteq \left\{{X},{Y},{Y}\right\}\right)\to {N}\left(\left\{{X},{Y}\right\}\right)\subseteq {N}\left(\left\{{X},{Y},{Y}\right\}\right)$
23 12 18 21 22 syl3anc ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\subseteq {N}\left(\left\{{X},{Y},{Y}\right\}\right)$
24 23 ssneld ${⊢}{\phi }\to \left(¬{z}\in {N}\left(\left\{{X},{Y},{Y}\right\}\right)\to ¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)$
25 24 reximdv ${⊢}{\phi }\to \left(\exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y},{Y}\right\}\right)\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)$
26 11 25 mpd ${⊢}{\phi }\to \exists {z}\in {V}\phantom{\rule{.4em}{0ex}}¬{z}\in {N}\left(\left\{{X},{Y}\right\}\right)$