Metamath Proof Explorer

Theorem hdmaplem3

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.y ${⊢}{\phi }\to {Y}\in {V}$
hdmaplem3.o
Assertion hdmaplem3

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.y ${⊢}{\phi }\to {Y}\in {V}$
7 hdmaplem3.o
8 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
9 1 8 2 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
10 3 6 9 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
11 elun2 ${⊢}{Z}\in {N}\left(\left\{{Y}\right\}\right)\to {Z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{Y}\right\}\right)\right)$
12 5 11 nsyl ${⊢}{\phi }\to ¬{Z}\in {N}\left(\left\{{Y}\right\}\right)$
13 7 8 3 10 4 12 lssneln0