Theorem lspexchn2

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 24-May-2015)

	Ref	Expression
Hypotheses	lspexchn2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspexchn2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspexchn2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspexchn2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspexchn2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspexchn2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	lspexchn2.q	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 } ) )
	lspexchn2.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) )
Assertion	lspexchn2	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspexchn2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspexchn2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lspexchn2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
4		lspexchn2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5		lspexchn2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6		lspexchn2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
7		lspexchn2.q	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 } ) )
8		lspexchn2.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) )
9		prcom	⊢ { 𝑍 , 𝑌 } = { 𝑌 , 𝑍 }
10	9	fveq2i	⊢ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , 𝑍 } )
11	10	eleq2i	⊢ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , 𝑌 } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
12	8 11	sylnib	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
13	1 2 3 4 5 6 7 12	lspexchn1	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
14		prcom	⊢ { 𝑋 , 𝑍 } = { 𝑍 , 𝑋 }
15	14	fveq2i	⊢ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) = ( 𝑁 ‘ { 𝑍 , 𝑋 } )
16	15	eleq2i	⊢ ( 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑋 } ) )
17	13 16	sylnib	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑋 } ) )