obslbs

Description: An orthogonal basis is a linear basis iff the span of the basis elements is closed (which is usually not true). (Contributed by Mario Carneiro, 29-Oct-2015)

	Ref	Expression
Hypotheses	obslbs.j	$⊢ J = LBasis (W)$
	obslbs.n	$⊢ N = LSpan (W)$
	obslbs.c	$⊢ C = ClSubSp (W)$
Assertion	obslbs	$⊢ B \in OBasis (W) \to (B \in J \leftrightarrow N (B) \in C)$

Proof

Step	Hyp	Ref	Expression
1		obslbs.j	$⊢ J = LBasis (W)$
2		obslbs.n	$⊢ N = LSpan (W)$
3		obslbs.c	$⊢ C = ClSubSp (W)$
4		obsrcl	$⊢ B \in OBasis (W) \to W \in PreHil$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6	5	obsss	$⊢ B \in OBasis (W) \to B \subseteq {Base}_{W}$
7		eqid	$⊢ ocv (W) = ocv (W)$
8	5 7 2	ocvlsp	$⊢ (W \in PreHil \land B \subseteq {Base}_{W}) \to ocv (W) (N (B)) = ocv (W) (B)$
9	4 6 8	syl2anc	$⊢ B \in OBasis (W) \to ocv (W) (N (B)) = ocv (W) (B)$
10	9	fveq2d	$⊢ B \in OBasis (W) \to ocv (W) (ocv (W) (N (B))) = ocv (W) (ocv (W) (B))$
11	7 5	obs2ocv	$⊢ B \in OBasis (W) \to ocv (W) (ocv (W) (B)) = {Base}_{W}$
12	10 11	eqtrd	$⊢ B \in OBasis (W) \to ocv (W) (ocv (W) (N (B))) = {Base}_{W}$
13	12	eqeq2d	$⊢ B \in OBasis (W) \to (N (B) = ocv (W) (ocv (W) (N (B))) \leftrightarrow N (B) = {Base}_{W})$
14	7 3	iscss	$⊢ W \in PreHil \to (N (B) \in C \leftrightarrow N (B) = ocv (W) (ocv (W) (N (B))))$
15	4 14	syl	$⊢ B \in OBasis (W) \to (N (B) \in C \leftrightarrow N (B) = ocv (W) (ocv (W) (N (B))))$
16		phllvec	$⊢ W \in PreHil \to W \in LVec$
17	4 16	syl	$⊢ B \in OBasis (W) \to W \in LVec$
18		pssnel	$⊢ x \subset B \to \exists y (y \in B \land \neg y \in x)$
19	18	adantl	$⊢ (B \in OBasis (W) \land x \subset B) \to \exists y (y \in B \land \neg y \in x)$
20		simpll	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to B \in OBasis (W)$
21		pssss	$⊢ x \subset B \to x \subseteq B$
22	21	ad2antlr	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to x \subseteq B$
23		simpr	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to y \in B$
24	7	obselocv	$⊢ (B \in OBasis (W) \land x \subseteq B \land y \in B) \to (y \in ocv (W) (x) \leftrightarrow \neg y \in x)$
25	20 22 23 24	syl3anc	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (y \in ocv (W) (x) \leftrightarrow \neg y \in x)$
26		eqid	$⊢ 0_{W} = 0_{W}$
27	26	obsne0	$⊢ (B \in OBasis (W) \land y \in B) \to y \neq 0_{W}$
28	20 23 27	syl2anc	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to y \neq 0_{W}$
29		nelsn	$⊢ y \neq 0_{W} \to \neg y \in \{0_{W}\}$
30	28 29	syl	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to \neg y \in \{0_{W}\}$
31		nelne1	$⊢ (y \in ocv (W) (x) \land \neg y \in \{0_{W}\}) \to ocv (W) (x) \neq \{0_{W}\}$
32	31	expcom	$⊢ \neg y \in \{0_{W}\} \to (y \in ocv (W) (x) \to ocv (W) (x) \neq \{0_{W}\})$
33	30 32	syl	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (y \in ocv (W) (x) \to ocv (W) (x) \neq \{0_{W}\})$
34	25 33	sylbird	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (\neg y \in x \to ocv (W) (x) \neq \{0_{W}\})$
35		npss	$⊢ \neg N (x) \subset {Base}_{W} \leftrightarrow (N (x) \subseteq {Base}_{W} \to N (x) = {Base}_{W})$
36		phllmod	$⊢ W \in PreHil \to W \in LMod$
37	4 36	syl	$⊢ B \in OBasis (W) \to W \in LMod$
38	37	ad2antrr	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to W \in LMod$
39	6	ad2antrr	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to B \subseteq {Base}_{W}$
40	22 39	sstrd	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to x \subseteq {Base}_{W}$
41	5 2	lspssv	$⊢ (W \in LMod \land x \subseteq {Base}_{W}) \to N (x) \subseteq {Base}_{W}$
42	38 40 41	syl2anc	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to N (x) \subseteq {Base}_{W}$
43		fveq2	$⊢ N (x) = {Base}_{W} \to ocv (W) (N (x)) = ocv (W) ({Base}_{W})$
44	4	ad2antrr	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to W \in PreHil$
45	5 7 2	ocvlsp	$⊢ (W \in PreHil \land x \subseteq {Base}_{W}) \to ocv (W) (N (x)) = ocv (W) (x)$
46	44 40 45	syl2anc	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to ocv (W) (N (x)) = ocv (W) (x)$
47	5 7 26	ocv1	$⊢ W \in PreHil \to ocv (W) ({Base}_{W}) = \{0_{W}\}$
48	44 47	syl	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to ocv (W) ({Base}_{W}) = \{0_{W}\}$
49	46 48	eqeq12d	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (ocv (W) (N (x)) = ocv (W) ({Base}_{W}) \leftrightarrow ocv (W) (x) = \{0_{W}\})$
50	43 49	syl5ib	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (N (x) = {Base}_{W} \to ocv (W) (x) = \{0_{W}\})$
51	42 50	embantd	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to ((N (x) \subseteq {Base}_{W} \to N (x) = {Base}_{W}) \to ocv (W) (x) = \{0_{W}\})$
52	35 51	syl5bi	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (\neg N (x) \subset {Base}_{W} \to ocv (W) (x) = \{0_{W}\})$
53	52	necon1ad	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (ocv (W) (x) \neq \{0_{W}\} \to N (x) \subset {Base}_{W})$
54	34 53	syld	$⊢ ((B \in OBasis (W) \land x \subset B) \land y \in B) \to (\neg y \in x \to N (x) \subset {Base}_{W})$
55	54	expimpd	$⊢ (B \in OBasis (W) \land x \subset B) \to ((y \in B \land \neg y \in x) \to N (x) \subset {Base}_{W})$
56	55	exlimdv	$⊢ (B \in OBasis (W) \land x \subset B) \to (\exists y (y \in B \land \neg y \in x) \to N (x) \subset {Base}_{W})$
57	19 56	mpd	$⊢ (B \in OBasis (W) \land x \subset B) \to N (x) \subset {Base}_{W}$
58	57	ex	$⊢ B \in OBasis (W) \to (x \subset B \to N (x) \subset {Base}_{W})$
59	58	alrimiv	$⊢ B \in OBasis (W) \to \forall x (x \subset B \to N (x) \subset {Base}_{W})$
60	5 1 2	islbs3	$⊢ W \in LVec \to (B \in J \leftrightarrow (B \subseteq {Base}_{W} \land N (B) = {Base}_{W} \land \forall x (x \subset B \to N (x) \subset {Base}_{W})))$
61		3anan32	$⊢ (B \subseteq {Base}_{W} \land N (B) = {Base}_{W} \land \forall x (x \subset B \to N (x) \subset {Base}_{W})) \leftrightarrow ((B \subseteq {Base}_{W} \land \forall x (x \subset B \to N (x) \subset {Base}_{W})) \land N (B) = {Base}_{W})$
62	60 61	bitrdi	$⊢ W \in LVec \to (B \in J \leftrightarrow ((B \subseteq {Base}_{W} \land \forall x (x \subset B \to N (x) \subset {Base}_{W})) \land N (B) = {Base}_{W}))$
63	62	baibd	$⊢ (W \in LVec \land (B \subseteq {Base}_{W} \land \forall x (x \subset B \to N (x) \subset {Base}_{W}))) \to (B \in J \leftrightarrow N (B) = {Base}_{W})$
64	17 6 59 63	syl12anc	$⊢ B \in OBasis (W) \to (B \in J \leftrightarrow N (B) = {Base}_{W})$
65	13 15 64	3bitr4rd	$⊢ B \in OBasis (W) \to (B \in J \leftrightarrow N (B) \in C)$

Metamath Proof Explorer

Theorem obslbs

Proof