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	|- .0. = ( 0g ` W )
	hdmaplem4.w	|- ( ph -> W e. LVec )
	hdmaplem4.x	|- ( ph -> X e. V )
	hdmaplem4.y	|- ( ph -> Y e. V )
	hdmaplem4.z	|- ( ph -> Z e. ( V \ { .0. } ) )
	hdmaplem4.e	|- ( ph -> ( N ` { Z } ) =/= ( N ` { X } ) )
	hdmaplem4.f	|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
Assertion	hdmaplem4	|- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaplem1.v	|- V = ( Base ` W )
2		hdmaplem1.n	|- N = ( LSpan ` W )
3		hdmaplem4.o	|- .0. = ( 0g ` W )
4		hdmaplem4.w	|- ( ph -> W e. LVec )
5		hdmaplem4.x	|- ( ph -> X e. V )
6		hdmaplem4.y	|- ( ph -> Y e. V )
7		hdmaplem4.z	|- ( ph -> Z e. ( V \ { .0. } ) )
8		hdmaplem4.e	|- ( ph -> ( N ` { Z } ) =/= ( N ` { X } ) )
9		hdmaplem4.f	|- ( ph -> ( N ` { Z } ) =/= ( N ` { Y } ) )
10	1 3 2 4 7 5 8	lspsnne1	|- ( ph -> -. Z e. ( N ` { X } ) )
11	1 3 2 4 7 6 9	lspsnne1	|- ( ph -> -. Z e. ( N ` { Y } ) )
12		ioran	|- ( -. ( Z e. ( N ` { X } ) \/ Z e. ( N ` { Y } ) ) <-> ( -. Z e. ( N ` { X } ) /\ -. Z e. ( N ` { Y } ) ) )
13		elun	|- ( Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) <-> ( Z e. ( N ` { X } ) \/ Z e. ( N ` { Y } ) ) )
14	12 13	xchnxbir	|- ( -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) <-> ( -. Z e. ( N ` { X } ) /\ -. Z e. ( N ` { Y } ) ) )
15	10 11 14	sylanbrc	|- ( ph -> -. Z e. ( ( N ` { X } ) u. ( N ` { Y } ) ) )