Metamath Proof Explorer

Theorem obsne0

Description: A basis element is nonzero. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypothesis obsocv.z ⊢ 0 ˙ = 0 W
Assertion obsne0 ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ≠ 0 ˙

Proof

Step Hyp Ref Expression
1 obsocv.z ⊢ 0 ˙ = 0 W
2 obsrcl ⊢ B ∈ OBasis ⁡ W → W ∈ PreHil
3 phllvec ⊢ W ∈ PreHil → W ∈ LVec
4 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
5 4 lvecdrng ⊢ W ∈ LVec → Scalar ⁡ W ∈ DivRing
6 2 3 5 3syl ⊢ B ∈ OBasis ⁡ W → Scalar ⁡ W ∈ DivRing
7 6 adantr ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → Scalar ⁡ W ∈ DivRing
8 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
9 eqid ⊢ 1 Scalar ⁡ W = 1 Scalar ⁡ W
10 8 9 drngunz ⊢ Scalar ⁡ W ∈ DivRing → 1 Scalar ⁡ W ≠ 0 Scalar ⁡ W
11 7 10 syl ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → 1 Scalar ⁡ W ≠ 0 Scalar ⁡ W
12 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
13 12 4 9 obsipid ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ⋅ 𝑖 ⁡ W A = 1 Scalar ⁡ W
14 13 eqeq1d ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ⋅ 𝑖 ⁡ W A = 0 Scalar ⁡ W ↔ 1 Scalar ⁡ W = 0 Scalar ⁡ W
15 eqid ⊢ Base W = Base W
16 15 obsss ⊢ B ∈ OBasis ⁡ W → B ⊆ Base W
17 16 sselda ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ∈ Base W
18 4 12 15 8 1 ipeq0 ⊢ W ∈ PreHil ∧ A ∈ Base W → A ⋅ 𝑖 ⁡ W A = 0 Scalar ⁡ W ↔ A = 0 ˙
19 2 17 18 syl2an2r ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ⋅ 𝑖 ⁡ W A = 0 Scalar ⁡ W ↔ A = 0 ˙
20 14 19 bitr3d ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → 1 Scalar ⁡ W = 0 Scalar ⁡ W ↔ A = 0 ˙
21 20 necon3bid ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → 1 Scalar ⁡ W ≠ 0 Scalar ⁡ W ↔ A ≠ 0 ˙
22 11 21 mpbid ⊢ B ∈ OBasis ⁡ W ∧ A ∈ B → A ≠ 0 ˙