islbs

Description: The predicate " B is a basis for the left module or vector space W ". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	islbs.v	$⊢ V = {Base}_{W}$
	islbs.f	$⊢ F = Scalar (W)$
	islbs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	islbs.k	$⊢ K = {Base}_{F}$
	islbs.j	$⊢ J = LBasis (W)$
	islbs.n	$⊢ N = LSpan (W)$
	islbs.z	$⊢ \underset{˙}{0} = 0_{F}$
Assertion	islbs	$⊢ W \in X \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$

Proof

Step	Hyp	Ref	Expression
1		islbs.v	$⊢ V = {Base}_{W}$
2		islbs.f	$⊢ F = Scalar (W)$
3		islbs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		islbs.k	$⊢ K = {Base}_{F}$
5		islbs.j	$⊢ J = LBasis (W)$
6		islbs.n	$⊢ N = LSpan (W)$
7		islbs.z	$⊢ \underset{˙}{0} = 0_{F}$
8		elex	$⊢ W \in X \to W \in V$
9		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
10	9 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
11	10	pweqd	$⊢ w = W \to 𝒫 {Base}_{w} = 𝒫 V$
12		fvexd	$⊢ w = W \to LSpan (w) \in V$
13		fveq2	$⊢ w = W \to LSpan (w) = LSpan (W)$
14	13 6	eqtr4di	$⊢ w = W \to LSpan (w) = N$
15		fvexd	$⊢ (w = W \land n = N) \to Scalar (w) \in V$
16		fveq2	$⊢ w = W \to Scalar (w) = Scalar (W)$
17	16	adantr	$⊢ (w = W \land n = N) \to Scalar (w) = Scalar (W)$
18	17 2	eqtr4di	$⊢ (w = W \land n = N) \to Scalar (w) = F$
19		simplr	$⊢ ((w = W \land n = N) \land f = F) \to n = N$
20	19	fveq1d	$⊢ ((w = W \land n = N) \land f = F) \to n (b) = N (b)$
21	10	ad2antrr	$⊢ ((w = W \land n = N) \land f = F) \to {Base}_{w} = V$
22	20 21	eqeq12d	$⊢ ((w = W \land n = N) \land f = F) \to (n (b) = {Base}_{w} \leftrightarrow N (b) = V)$
23		simpr	$⊢ ((w = W \land n = N) \land f = F) \to f = F$
24	23	fveq2d	$⊢ ((w = W \land n = N) \land f = F) \to {Base}_{f} = {Base}_{F}$
25	24 4	eqtr4di	$⊢ ((w = W \land n = N) \land f = F) \to {Base}_{f} = K$
26	23	fveq2d	$⊢ ((w = W \land n = N) \land f = F) \to 0_{f} = 0_{F}$
27	26 7	eqtr4di	$⊢ ((w = W \land n = N) \land f = F) \to 0_{f} = \underset{˙}{0}$
28	27	sneqd	$⊢ ((w = W \land n = N) \land f = F) \to \{0_{f}\} = \{\underset{˙}{0}\}$
29	25 28	difeq12d	$⊢ ((w = W \land n = N) \land f = F) \to {Base}_{f} ∖ \{0_{f}\} = K ∖ \{\underset{˙}{0}\}$
30		fveq2	$⊢ w = W \to \cdot_{w} = \cdot_{W}$
31	30 3	eqtr4di	$⊢ w = W \to \cdot_{w} = \underset{˙}{\cdot}$
32	31	ad2antrr	$⊢ ((w = W \land n = N) \land f = F) \to \cdot_{w} = \underset{˙}{\cdot}$
33	32	oveqd	$⊢ ((w = W \land n = N) \land f = F) \to y \cdot_{w} x = y \underset{˙}{\cdot} x$
34	19	fveq1d	$⊢ ((w = W \land n = N) \land f = F) \to n (b ∖ \{x\}) = N (b ∖ \{x\})$
35	33 34	eleq12d	$⊢ ((w = W \land n = N) \land f = F) \to (y \cdot_{w} x \in n (b ∖ \{x\}) \leftrightarrow y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))$
36	35	notbid	$⊢ ((w = W \land n = N) \land f = F) \to (\neg y \cdot_{w} x \in n (b ∖ \{x\}) \leftrightarrow \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))$
37	29 36	raleqbidv	$⊢ ((w = W \land n = N) \land f = F) \to (\forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\}) \leftrightarrow \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))$
38	37	ralbidv	$⊢ ((w = W \land n = N) \land f = F) \to (\forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\}) \leftrightarrow \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))$
39	22 38	anbi12d	$⊢ ((w = W \land n = N) \land f = F) \to ((n (b) = {Base}_{w} \land \forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\})) \leftrightarrow (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\})))$
40	15 18 39	sbcied2	$⊢ (w = W \land n = N) \to (\underset{˙}{[} Scalar (w) / f \underset{˙}{]} (n (b) = {Base}_{w} \land \forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\})) \leftrightarrow (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\})))$
41	12 14 40	sbcied2	$⊢ w = W \to (\underset{˙}{[} LSpan (w) / n \underset{˙}{]} \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (n (b) = {Base}_{w} \land \forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\})) \leftrightarrow (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\})))$
42	11 41	rabeqbidv	$⊢ w = W \to \{b \in 𝒫 {Base}_{w} \| \underset{˙}{[} LSpan (w) / n \underset{˙}{]} \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (n (b) = {Base}_{w} \land \forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\}))\} = \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\}$
43		df-lbs	$⊢ LBasis = (w \in V ⟼ \{b \in 𝒫 {Base}_{w} \| \underset{˙}{[} LSpan (w) / n \underset{˙}{]} \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (n (b) = {Base}_{w} \land \forall x \in b \forall y \in ({Base}_{f} ∖ \{0_{f}\}) \neg y \cdot_{w} x \in n (b ∖ \{x\}))\})$
44	1	fvexi	$⊢ V \in V$
45	44	pwex	$⊢ 𝒫 V \in V$
46	45	rabex	$⊢ \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\} \in V$
47	42 43 46	fvmpt	$⊢ W \in V \to LBasis (W) = \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\}$
48	5 47	syl5eq	$⊢ W \in V \to J = \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\}$
49	8 48	syl	$⊢ W \in X \to J = \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\}$
50	49	eleq2d	$⊢ W \in X \to (B \in J \leftrightarrow B \in \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\})$
51	44	elpw2	$⊢ B \in 𝒫 V \leftrightarrow B \subseteq V$
52	51	anbi1i	$⊢ (B \in 𝒫 V \land (N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))) \leftrightarrow (B \subseteq V \land (N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$
53		fveqeq2	$⊢ b = B \to (N (b) = V \leftrightarrow N (B) = V)$
54		difeq1	$⊢ b = B \to b ∖ \{x\} = B ∖ \{x\}$
55	54	fveq2d	$⊢ b = B \to N (b ∖ \{x\}) = N (B ∖ \{x\})$
56	55	eleq2d	$⊢ b = B \to (y \underset{˙}{\cdot} x \in N (b ∖ \{x\}) \leftrightarrow y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))$
57	56	notbid	$⊢ b = B \to (\neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}) \leftrightarrow \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))$
58	57	ralbidv	$⊢ b = B \to (\forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}) \leftrightarrow \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))$
59	58	raleqbi1dv	$⊢ b = B \to (\forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}) \leftrightarrow \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))$
60	53 59	anbi12d	$⊢ b = B \to ((N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\})) \leftrightarrow (N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$
61	60	elrab	$⊢ B \in \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\} \leftrightarrow (B \in 𝒫 V \land (N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$
62		3anass	$⊢ (B \subseteq V \land N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})) \leftrightarrow (B \subseteq V \land (N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$
63	52 61 62	3bitr4i	$⊢ B \in \{b \in 𝒫 V \| (N (b) = V \land \forall x \in b \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (b ∖ \{x\}))\} \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\}))$
64	50 63	bitrdi	$⊢ W \in X \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \forall y \in (K ∖ \{\underset{˙}{0}\}) \neg y \underset{˙}{\cdot} x \in N (B ∖ \{x\})))$

Metamath Proof Explorer

Theorem islbs

Proof