This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspsneq0b

Description: Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015)

Ref Expression
Hypotheses lspsneq0b.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsneq0b.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspsneq0b.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsneq0b.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsneq0b.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsneq0b.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspsneq0b.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
Assertion lspsneq0b ( 𝜑 → ( 𝑋 = 0 ↔ 𝑌 = 0 ) )

Proof

Step Hyp Ref Expression
1 lspsneq0b.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsneq0b.o ⊢ 0 = ( 0g ‘ 𝑊 )
3 lspsneq0b.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsneq0b.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lspsneq0b.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspsneq0b.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspsneq0b.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
9 1 2 3 lspsneq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
10 4 5 9 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
11 10 biimpar ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = { 0 } )
12 8 11 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑌 } ) = { 0 } )
13 1 2 3 lspsneq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑌 } ) = { 0 } ↔ 𝑌 = 0 ) )
14 4 6 13 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) = { 0 } ↔ 𝑌 = 0 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑁 ‘ { 𝑌 } ) = { 0 } ↔ 𝑌 = 0 ) )
16 12 15 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → 𝑌 = 0 )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
18 14 biimpar ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → ( 𝑁 ‘ { 𝑌 } ) = { 0 } )
19 17 18 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = { 0 } )
20 10 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
21 19 20 mpbid ⊢ ( ( 𝜑 ∧ 𝑌 = 0 ) → 𝑋 = 0 )
22 16 21 impbida ⊢ ( 𝜑 → ( 𝑋 = 0 ↔ 𝑌 = 0 ) )