Metamath Proof Explorer


Theorem lspexchn1

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, 20-May-2015)

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

Proof

Step Hyp Ref Expression
1 lspexchn1.v 𝑉 = ( Base ‘ 𝑊 )
2 lspexchn1.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lspexchn1.w ( 𝜑𝑊 ∈ LVec )
4 lspexchn1.x ( 𝜑𝑋𝑉 )
5 lspexchn1.y ( 𝜑𝑌𝑉 )
6 lspexchn1.z ( 𝜑𝑍𝑉 )
7 lspexchn1.q ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 } ) )
8 lspexchn1.e ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
9 eqid ( 0g𝑊 ) = ( 0g𝑊 )
10 3 adantr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑊 ∈ LVec )
11 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
12 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
13 3 12 syl ( 𝜑𝑊 ∈ LMod )
14 1 11 2 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑍𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
15 13 6 14 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
16 9 11 13 15 5 7 lssneln0 ( 𝜑𝑌 ∈ ( 𝑉 ∖ { ( 0g𝑊 ) } ) )
17 16 adantr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑌 ∈ ( 𝑉 ∖ { ( 0g𝑊 ) } ) )
18 4 adantr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑋𝑉 )
19 6 adantr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑍𝑉 )
20 1 2 13 5 6 7 lspsnne2 ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
21 20 adantr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
22 simpr ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
23 1 9 2 10 17 18 19 21 22 lspexch ( ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
24 8 23 mtand ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )