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	$$⊢V={\mathrm{Base}}_W$$
	lspsneq0b.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsneq0b.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspsneq0b.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspsneq0b.x	$$⊢\phi \to X\in V$$
	lspsneq0b.y	$$⊢\phi \to Y\in V$$
	lspsneq0b.e	$$⊢\phi \to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
Assertion	lspsneq0b	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsneq0b.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsneq0b.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspsneq0b.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspsneq0b.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspsneq0b.x	$$⊢\phi \to X\in V$$
6		lspsneq0b.y	$$⊢\phi \to Y\in V$$
7		lspsneq0b.e	$$⊢\phi \to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
8	7	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
9	1 2 3	lspsneq0	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
10	4 5 9	syl2anc	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
11	10	biimpar	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
12	8 11	eqtr3d	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
13	1 2 3	lspsneq0	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to \left(N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
14	4 6 13	syl2anc	$$⊢\phi \to \left(N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
15	14	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to \left(N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
16	12 15	mpbid	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{0}$$
17	7	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
18	14	biimpar	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to N\left(\left\{Y\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
19	17 18	eqtrd	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
20	10	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
21	19 20	mpbid	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to X=\underset{\dot{}}{0}$$
22	16 21	impbida	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$