obsne0

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

		Ref	Expression
	Hypothesis	obsocv.z	$⊢ \underset{˙}{0} = 0_{W}$
	Assertion	obsne0	$⊢ (B \in OBasis (W) \land A \in B) \to A \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		obsocv.z	$⊢ \underset{˙}{0} = 0_{W}$
2		obsrcl	$⊢ B \in OBasis (W) \to W \in PreHil$
3		phllvec	$⊢ W \in PreHil \to W \in LVec$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5	4	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
6	2 3 5	3syl	$⊢ B \in OBasis (W) \to Scalar (W) \in DivRing$
7	6	adantr	$⊢ (B \in OBasis (W) \land A \in B) \to Scalar (W) \in DivRing$
8		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
9		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
10	8 9	drngunz	$⊢ Scalar (W) \in DivRing \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
11	7 10	syl	$⊢ (B \in OBasis (W) \land A \in B) \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
12		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
13	12 4 9	obsipid	$⊢ (B \in OBasis (W) \land A \in B) \to A \cdot_{𝑖} (W) A = 1_{Scalar (W)}$
14	13	eqeq1d	$⊢ (B \in OBasis (W) \land A \in B) \to (A \cdot_{𝑖} (W) A = 0_{Scalar (W)} \leftrightarrow 1_{Scalar (W)} = 0_{Scalar (W)})$
15		eqid	$⊢ {Base}_{W} = {Base}_{W}$
16	15	obsss	$⊢ B \in OBasis (W) \to B \subseteq {Base}_{W}$
17	16	sselda	$⊢ (B \in OBasis (W) \land A \in B) \to A \in {Base}_{W}$
18	4 12 15 8 1	ipeq0	$⊢ (W \in PreHil \land A \in {Base}_{W}) \to (A \cdot_{𝑖} (W) A = 0_{Scalar (W)} \leftrightarrow A = \underset{˙}{0})$
19	2 17 18	syl2an2r	$⊢ (B \in OBasis (W) \land A \in B) \to (A \cdot_{𝑖} (W) A = 0_{Scalar (W)} \leftrightarrow A = \underset{˙}{0})$
20	14 19	bitr3d	$⊢ (B \in OBasis (W) \land A \in B) \to (1_{Scalar (W)} = 0_{Scalar (W)} \leftrightarrow A = \underset{˙}{0})$
21	20	necon3bid	$⊢ (B \in OBasis (W) \land A \in B) \to (1_{Scalar (W)} \neq 0_{Scalar (W)} \leftrightarrow A \neq \underset{˙}{0})$
22	11 21	mpbid	$⊢ (B \in OBasis (W) \land A \in B) \to A \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem obsne0

Proof