Metamath Proof Explorer

Theorem hdmaplem1

Description: Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmaplem1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
hdmaplem1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
hdmaplem1.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
hdmaplem1.z ${⊢}{\phi }\to {Z}\in {V}$
hdmaplem1.j ${⊢}{\phi }\to ¬{Z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{Y}\right\}\right)\right)$
hdmaplem1.x ${⊢}{\phi }\to {X}\in {V}$
Assertion hdmaplem1 ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$

Proof

Step Hyp Ref Expression
1 hdmaplem1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 hdmaplem1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 hdmaplem1.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
4 hdmaplem1.z ${⊢}{\phi }\to {Z}\in {V}$
5 hdmaplem1.j ${⊢}{\phi }\to ¬{Z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{Y}\right\}\right)\right)$
6 hdmaplem1.x ${⊢}{\phi }\to {X}\in {V}$
7 elun1 ${⊢}{Z}\in {N}\left(\left\{{X}\right\}\right)\to {Z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{Y}\right\}\right)\right)$
8 5 7 nsyl ${⊢}{\phi }\to ¬{Z}\in {N}\left(\left\{{X}\right\}\right)$
9 1 2 3 4 6 8 lspsnne2 ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$