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

Metamath Proof Explorer

Theorem shne0i

Description: A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis shne0.1 ⊢ 𝐴 ∈ Sℋ
Assertion shne0i ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )

Proof

Step Hyp Ref Expression
1 shne0.1 ⊢ 𝐴 ∈ Sℋ
2 df-ne ⊢ ( 𝐴 ≠ 0ℋ ↔ ¬ 𝐴 = 0ℋ )
3 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 0ℋ ) )
4 nss ⊢ ( ¬ 𝐴 ⊆ 0ℋ ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 0ℋ ) )
5 shle0 ⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )
6 1 5 ax-mp ⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
7 6 notbii ⊢ ( ¬ 𝐴 ⊆ 0ℋ ↔ ¬ 𝐴 = 0ℋ )
8 3 4 7 3bitr2ri ⊢ ( ¬ 𝐴 = 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ )
9 elch0 ⊢ ( 𝑥 ∈ 0ℋ ↔ 𝑥 = 0ℎ )
10 9 necon3bbii ⊢ ( ¬ 𝑥 ∈ 0ℋ ↔ 𝑥 ≠ 0ℎ )
11 10 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )
12 2 8 11 3bitri ⊢ ( 𝐴 ≠ 0ℋ ↔ ∃ 𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ )