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 ) )