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 = Base W
hdmaplem1.n N = LSpan W
hdmaplem1.w φ W LMod
hdmaplem1.z φ Z V
hdmaplem1.j φ ¬ Z N X N Y
hdmaplem1.x φ X V
Assertion hdmaplem1 φ N Z N X


Step Hyp Ref Expression
1 hdmaplem1.v V = Base W
2 hdmaplem1.n N = LSpan W
3 hdmaplem1.w φ W LMod
4 hdmaplem1.z φ Z V
5 hdmaplem1.j φ ¬ Z N X N Y
6 hdmaplem1.x φ X V
7 elun1 Z N X Z N X N Y
8 5 7 nsyl φ ¬ Z N X
9 1 2 3 4 6 8 lspsnne2 φ N Z N X