Theorem obsne0

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

	Ref	Expression
Hypothesis	obsocv.z	|- .0. = ( 0g ` W )
Assertion	obsne0	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> A =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		obsocv.z	|- .0. = ( 0g ` W )
2		obsrcl	|- ( B e. ( OBasis ` W ) -> W e. PreHil )
3		phllvec	|- ( W e. PreHil -> W e. LVec )
4		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
5	4	lvecdrng	|- ( W e. LVec -> ( Scalar ` W ) e. DivRing )
6	2 3 5	3syl	|- ( B e. ( OBasis ` W ) -> ( Scalar ` W ) e. DivRing )
7	6	adantr	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( Scalar ` W ) e. DivRing )
8		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
9		eqid	|- ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
10	8 9	drngunz	|- ( ( Scalar ` W ) e. DivRing -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
11	7 10	syl	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
12		eqid	|- ( .i ` W ) = ( .i ` W )
13	12 4 9	obsipid	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( A ( .i ` W ) A ) = ( 1r ` ( Scalar ` W ) ) )
14	13	eqeq1d	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( ( A ( .i ` W ) A ) = ( 0g ` ( Scalar ` W ) ) <-> ( 1r ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) ) )
15		eqid	|- ( Base ` W ) = ( Base ` W )
16	15	obsss	|- ( B e. ( OBasis ` W ) -> B C_ ( Base ` W ) )
17	16	sselda	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> A e. ( Base ` W ) )
18	4 12 15 8 1	ipeq0	|- ( ( W e. PreHil /\ A e. ( Base ` W ) ) -> ( ( A ( .i ` W ) A ) = ( 0g ` ( Scalar ` W ) ) <-> A = .0. ) )
19	2 17 18	syl2an2r	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( ( A ( .i ` W ) A ) = ( 0g ` ( Scalar ` W ) ) <-> A = .0. ) )
20	14 19	bitr3d	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( ( 1r ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) <-> A = .0. ) )
21	20	necon3bid	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) <-> A =/= .0. ) )
22	11 21	mpbid	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> A =/= .0. )