Theorem obsne0

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

	Ref	Expression
Hypothesis	obsocv.z	⊢ 0 = ( 0g ‘ 𝑊 )
Assertion	obsne0	⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ≠ 0 )

Proof

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