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 ⊢ V = Base W
lspsneq0b.o ⊢ 0 ˙ = 0 W
lspsneq0b.n ⊢ N = LSpan ⁡ W
lspsneq0b.w ⊢ φ → W ∈ LMod
lspsneq0b.x ⊢ φ → X ∈ V
lspsneq0b.y ⊢ φ → Y ∈ V
lspsneq0b.e ⊢ φ → N ⁡ X = N ⁡ Y
Assertion lspsneq0b ⊢ φ → X = 0 ˙ ↔ Y = 0 ˙

Proof

Step Hyp Ref Expression
1 lspsneq0b.v ⊢ V = Base W
2 lspsneq0b.o ⊢ 0 ˙ = 0 W
3 lspsneq0b.n ⊢ N = LSpan ⁡ W
4 lspsneq0b.w ⊢ φ → W ∈ LMod
5 lspsneq0b.x ⊢ φ → X ∈ V
6 lspsneq0b.y ⊢ φ → Y ∈ V
7 lspsneq0b.e ⊢ φ → N ⁡ X = N ⁡ Y
8 7 adantr ⊢ φ ∧ X = 0 ˙ → N ⁡ X = N ⁡ Y
9 1 2 3 lspsneq0 ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X = 0 ˙ ↔ X = 0 ˙
10 4 5 9 syl2anc ⊢ φ → N ⁡ X = 0 ˙ ↔ X = 0 ˙
11 10 biimpar ⊢ φ ∧ X = 0 ˙ → N ⁡ X = 0 ˙
12 8 11 eqtr3d ⊢ φ ∧ X = 0 ˙ → N ⁡ Y = 0 ˙
13 1 2 3 lspsneq0 ⊢ W ∈ LMod ∧ Y ∈ V → N ⁡ Y = 0 ˙ ↔ Y = 0 ˙
14 4 6 13 syl2anc ⊢ φ → N ⁡ Y = 0 ˙ ↔ Y = 0 ˙
15 14 adantr ⊢ φ ∧ X = 0 ˙ → N ⁡ Y = 0 ˙ ↔ Y = 0 ˙
16 12 15 mpbid ⊢ φ ∧ X = 0 ˙ → Y = 0 ˙
17 7 adantr ⊢ φ ∧ Y = 0 ˙ → N ⁡ X = N ⁡ Y
18 14 biimpar ⊢ φ ∧ Y = 0 ˙ → N ⁡ Y = 0 ˙
19 17 18 eqtrd ⊢ φ ∧ Y = 0 ˙ → N ⁡ X = 0 ˙
20 10 adantr ⊢ φ ∧ Y = 0 ˙ → N ⁡ X = 0 ˙ ↔ X = 0 ˙
21 19 20 mpbid ⊢ φ ∧ Y = 0 ˙ → X = 0 ˙
22 16 21 impbida ⊢ φ → X = 0 ˙ ↔ Y = 0 ˙