lsslindf

Description: Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	lsslindf.u	$⊢ U = LSubSp (W)$
	lsslindf.x	$⊢ X = W ↾_{𝑠} S$
Assertion	lsslindf	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F LIndF X \leftrightarrow F LIndF W)$

Proof

Step	Hyp	Ref	Expression
1		lsslindf.u	$⊢ U = LSubSp (W)$
2		lsslindf.x	$⊢ X = W ↾_{𝑠} S$
3		rellindf	$⊢ Rel LIndF$
4	3	brrelex1i	$⊢ F LIndF X \to F \in V$
5	4	a1i	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F LIndF X \to F \in V)$
6	3	brrelex1i	$⊢ F LIndF W \to F \in V$
7	6	a1i	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F LIndF W \to F \in V)$
8		simpr	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F : dom F ⟶ {Base}_{X}) \to F : dom F ⟶ {Base}_{X}$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10	2 9	ressbasss	$⊢ {Base}_{X} \subseteq {Base}_{W}$
11		fss	$⊢ (F : dom F ⟶ {Base}_{X} \land {Base}_{X} \subseteq {Base}_{W}) \to F : dom F ⟶ {Base}_{W}$
12	8 10 11	sylancl	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F : dom F ⟶ {Base}_{X}) \to F : dom F ⟶ {Base}_{W}$
13		ffn	$⊢ F : dom F ⟶ {Base}_{W} \to F Fn dom F$
14	13	adantl	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F : dom F ⟶ {Base}_{W}) \to F Fn dom F$
15		simp3	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to ran F \subseteq S$
16	9 1	lssss	$⊢ S \in U \to S \subseteq {Base}_{W}$
17	16	3ad2ant2	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to S \subseteq {Base}_{W}$
18	2 9	ressbas2	$⊢ S \subseteq {Base}_{W} \to S = {Base}_{X}$
19	17 18	syl	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to S = {Base}_{X}$
20	15 19	sseqtrd	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to ran F \subseteq {Base}_{X}$
21	20	adantr	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F : dom F ⟶ {Base}_{W}) \to ran F \subseteq {Base}_{X}$
22		df-f	$⊢ F : dom F ⟶ {Base}_{X} \leftrightarrow (F Fn dom F \land ran F \subseteq {Base}_{X})$
23	14 21 22	sylanbrc	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F : dom F ⟶ {Base}_{W}) \to F : dom F ⟶ {Base}_{X}$
24	12 23	impbida	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F : dom F ⟶ {Base}_{X} \leftrightarrow F : dom F ⟶ {Base}_{W})$
25	24	adantr	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (F : dom F ⟶ {Base}_{X} \leftrightarrow F : dom F ⟶ {Base}_{W})$
26		simpl2	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to S \in U$
27		eqid	$⊢ Scalar (W) = Scalar (W)$
28	2 27	resssca	$⊢ S \in U \to Scalar (W) = Scalar (X)$
29	28	eqcomd	$⊢ S \in U \to Scalar (X) = Scalar (W)$
30	26 29	syl	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to Scalar (X) = Scalar (W)$
31	30	fveq2d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to {Base}_{Scalar (X)} = {Base}_{Scalar (W)}$
32	30	fveq2d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to 0_{Scalar (X)} = 0_{Scalar (W)}$
33	32	sneqd	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to \{0_{Scalar (X)}\} = \{0_{Scalar (W)}\}$
34	31 33	difeq12d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to {Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\} = {Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}$
35		eqid	$⊢ \cdot_{W} = \cdot_{W}$
36	2 35	ressvsca	$⊢ S \in U \to \cdot_{W} = \cdot_{X}$
37	36	eqcomd	$⊢ S \in U \to \cdot_{X} = \cdot_{W}$
38	26 37	syl	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to \cdot_{X} = \cdot_{W}$
39	38	oveqd	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to k \cdot_{X} F (x) = k \cdot_{W} F (x)$
40		simpl1	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to W \in LMod$
41		imassrn	$⊢ F [dom F ∖ \{x\}] \subseteq ran F$
42		simpl3	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to ran F \subseteq S$
43	41 42	sstrid	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to F [dom F ∖ \{x\}] \subseteq S$
44		eqid	$⊢ LSpan (W) = LSpan (W)$
45		eqid	$⊢ LSpan (X) = LSpan (X)$
46	2 44 45 1	lsslsp	$⊢ (W \in LMod \land S \in U \land F [dom F ∖ \{x\}] \subseteq S) \to LSpan (W) (F [dom F ∖ \{x\}]) = LSpan (X) (F [dom F ∖ \{x\}])$
47	40 26 43 46	syl3anc	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to LSpan (W) (F [dom F ∖ \{x\}]) = LSpan (X) (F [dom F ∖ \{x\}])$
48	47	eqcomd	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to LSpan (X) (F [dom F ∖ \{x\}]) = LSpan (W) (F [dom F ∖ \{x\}])$
49	39 48	eleq12d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}]) \leftrightarrow k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}]))$
50	49	notbid	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (\neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}]) \leftrightarrow \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}]))$
51	34 50	raleqbidv	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (\forall k \in ({Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\}) \neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}]) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}]))$
52	51	ralbidv	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (\forall x \in dom F \forall k \in ({Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\}) \neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}]) \leftrightarrow \forall x \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}]))$
53	25 52	anbi12d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to ((F : dom F ⟶ {Base}_{X} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\}) \neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}])) \leftrightarrow (F : dom F ⟶ {Base}_{W} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}])))$
54	2	ovexi	$⊢ X \in V$
55	54	a1i	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to X \in V$
56		eqid	$⊢ {Base}_{X} = {Base}_{X}$
57		eqid	$⊢ \cdot_{X} = \cdot_{X}$
58		eqid	$⊢ Scalar (X) = Scalar (X)$
59		eqid	$⊢ {Base}_{Scalar (X)} = {Base}_{Scalar (X)}$
60		eqid	$⊢ 0_{Scalar (X)} = 0_{Scalar (X)}$
61	56 57 45 58 59 60	islindf	$⊢ (X \in V \land F \in V) \to (F LIndF X \leftrightarrow (F : dom F ⟶ {Base}_{X} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\}) \neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}])))$
62	55 61	sylan	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (F LIndF X \leftrightarrow (F : dom F ⟶ {Base}_{X} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (X)} ∖ \{0_{Scalar (X)}\}) \neg k \cdot_{X} F (x) \in LSpan (X) (F [dom F ∖ \{x\}])))$
63		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
64		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
65	9 35 44 27 63 64	islindf	$⊢ (W \in LMod \land F \in V) \to (F LIndF W \leftrightarrow (F : dom F ⟶ {Base}_{W} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}])))$
66	65	3ad2antl1	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (F LIndF W \leftrightarrow (F : dom F ⟶ {Base}_{W} \land \forall x \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (x) \in LSpan (W) (F [dom F ∖ \{x\}])))$
67	53 62 66	3bitr4d	$⊢ ((W \in LMod \land S \in U \land ran F \subseteq S) \land F \in V) \to (F LIndF X \leftrightarrow F LIndF W)$
68	67	ex	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F \in V \to (F LIndF X \leftrightarrow F LIndF W))$
69	5 7 68	pm5.21ndd	$⊢ (W \in LMod \land S \in U \land ran F \subseteq S) \to (F LIndF X \leftrightarrow F LIndF W)$

Metamath Proof Explorer

Theorem lsslindf

Proof