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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	hdmaplem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	hdmaplem4.o	⊢ 0 = ( 0g ‘ 𝑊 )
	hdmaplem4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	hdmaplem4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmaplem4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	hdmaplem4.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
	hdmaplem4.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
	hdmaplem4.f	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion	hdmaplem4	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaplem1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		hdmaplem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		hdmaplem4.o	⊢ 0 = ( 0g ‘ 𝑊 )
4		hdmaplem4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		hdmaplem4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		hdmaplem4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		hdmaplem4.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
8		hdmaplem4.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
9		hdmaplem4.f	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
10	1 3 2 4 7 5 8	lspsnne1	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 } ) )
11	1 3 2 4 7 6 9	lspsnne1	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) )
12		ioran	⊢ ( ¬ ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
13		elun	⊢ ( 𝑍 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 } ) ∨ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
14	12 13	xchnxbir	⊢ ( ¬ 𝑍 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
15	10 11 14	sylanbrc	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) )