Metamath Proof Explorer

Theorem hdmaplem4

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)$
		hdmaplem4.o	$⊢ \underset{˙}{0} = 0_{W}$
		hdmaplem4.w	$⊢ φ \to W \in LVec$
		hdmaplem4.x	$⊢ φ \to X \in V$
		hdmaplem4.y	$⊢ φ \to Y \in V$
		hdmaplem4.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
		hdmaplem4.e	$⊢ φ \to N (\{Z\}) \neq N (\{X\})$
		hdmaplem4.f	$⊢ φ \to N (\{Z\}) \neq N (\{Y\})$
	Assertion	hdmaplem4	$⊢ φ \to \neg Z \in (N (\{X\}) \cup N (\{Y\}))$

Proof

Step	Hyp	Ref	Expression
1		hdmaplem1.v	$⊢ V = {Base}_{W}$
2		hdmaplem1.n	$⊢ N = LSpan (W)$
3		hdmaplem4.o	$⊢ \underset{˙}{0} = 0_{W}$
4		hdmaplem4.w	$⊢ φ \to W \in LVec$
5		hdmaplem4.x	$⊢ φ \to X \in V$
6		hdmaplem4.y	$⊢ φ \to Y \in V$
7		hdmaplem4.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
8		hdmaplem4.e	$⊢ φ \to N (\{Z\}) \neq N (\{X\})$
9		hdmaplem4.f	$⊢ φ \to N (\{Z\}) \neq N (\{Y\})$
10	1 3 2 4 7 5 8	lspsnne1	$⊢ φ \to \neg Z \in N (\{X\})$
11	1 3 2 4 7 6 9	lspsnne1	$⊢ φ \to \neg Z \in N (\{Y\})$
12		ioran	$⊢ \neg (Z \in N (\{X\}) \lor Z \in N (\{Y\})) \leftrightarrow (\neg Z \in N (\{X\}) \land \neg Z \in N (\{Y\}))$
13		elun	$⊢ Z \in (N (\{X\}) \cup N (\{Y\})) \leftrightarrow (Z \in N (\{X\}) \lor Z \in N (\{Y\}))$
14	12 13	xchnxbir	$⊢ \neg Z \in (N (\{X\}) \cup N (\{Y\})) \leftrightarrow (\neg Z \in N (\{X\}) \land \neg Z \in N (\{Y\}))$
15	10 11 14	sylanbrc	$⊢ φ \to \neg Z \in (N (\{X\}) \cup N (\{Y\}))$