lindfmm

Description: Linear independence of a family is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	lindfmm.b	$⊢ B = {Base}_{S}$
	lindfmm.c	$⊢ C = {Base}_{T}$
Assertion	lindfmm	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (F LIndF S \leftrightarrow (G \circ F) LIndF T)$

Proof

Step	Hyp	Ref	Expression
1		lindfmm.b	$⊢ B = {Base}_{S}$
2		lindfmm.c	$⊢ C = {Base}_{T}$
3		rellindf	$⊢ Rel LIndF$
4	3	brrelex1i	$⊢ F LIndF S \to F \in V$
5		simp3	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to F : I ⟶ B$
6		dmfex	$⊢ (F \in V \land F : I ⟶ B) \to I \in V$
7	4 5 6	syl2anr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \land F LIndF S) \to I \in V$
8	7	ex	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (F LIndF S \to I \in V)$
9	3	brrelex1i	$⊢ (G \circ F) LIndF T \to G \circ F \in V$
10		f1f	$⊢ G : B \underset{1-1}{⟶} C \to G : B ⟶ C$
11		fco	$⊢ (G : B ⟶ C \land F : I ⟶ B) \to (G \circ F) : I ⟶ C$
12	10 11	sylan	$⊢ (G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (G \circ F) : I ⟶ C$
13	12	3adant1	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (G \circ F) : I ⟶ C$
14		dmfex	$⊢ (G \circ F \in V \land (G \circ F) : I ⟶ C) \to I \in V$
15	9 13 14	syl2anr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \land (G \circ F) LIndF T) \to I \in V$
16	15	ex	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to ((G \circ F) LIndF T \to I \in V)$
17		eldifi	$⊢ k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \to k \in {Base}_{Scalar (S)}$
18		simpllr	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G : B \underset{1-1}{⟶} C$
19		lmhmlmod1	$⊢ G \in (S LMHom T) \to S \in LMod$
20	19	ad3antrrr	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to S \in LMod$
21		simprr	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to k \in {Base}_{Scalar (S)}$
22		simprl	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to F : I ⟶ B$
23		simpl	$⊢ (x \in I \land k \in {Base}_{Scalar (S)}) \to x \in I$
24		ffvelcdm	$⊢ (F : I ⟶ B \land x \in I) \to F (x) \in B$
25	22 23 24	syl2an	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to F (x) \in B$
26		eqid	$⊢ Scalar (S) = Scalar (S)$
27		eqid	$⊢ \cdot_{S} = \cdot_{S}$
28		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
29	1 26 27 28	lmodvscl	$⊢ (S \in LMod \land k \in {Base}_{Scalar (S)} \land F (x) \in B) \to k \cdot_{S} F (x) \in B$
30	20 21 25 29	syl3anc	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to k \cdot_{S} F (x) \in B$
31		imassrn	$⊢ F [I ∖ \{x\}] \subseteq ran F$
32		frn	$⊢ F : I ⟶ B \to ran F \subseteq B$
33	32	adantr	$⊢ (F : I ⟶ B \land I \in V) \to ran F \subseteq B$
34	31 33	sstrid	$⊢ (F : I ⟶ B \land I \in V) \to F [I ∖ \{x\}] \subseteq B$
35	34	ad2antlr	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to F [I ∖ \{x\}] \subseteq B$
36		eqid	$⊢ LSpan (S) = LSpan (S)$
37	1 36	lspssv	$⊢ (S \in LMod \land F [I ∖ \{x\}] \subseteq B) \to LSpan (S) (F [I ∖ \{x\}]) \subseteq B$
38	20 35 37	syl2anc	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to LSpan (S) (F [I ∖ \{x\}]) \subseteq B$
39		f1elima	$⊢ (G : B \underset{1-1}{⟶} C \land k \cdot_{S} F (x) \in B \land LSpan (S) (F [I ∖ \{x\}]) \subseteq B) \to (G (k \cdot_{S} F (x)) \in G [LSpan (S) (F [I ∖ \{x\}])] \leftrightarrow k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]))$
40	18 30 38 39	syl3anc	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to (G (k \cdot_{S} F (x)) \in G [LSpan (S) (F [I ∖ \{x\}])] \leftrightarrow k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]))$
41		simplll	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G \in (S LMHom T)$
42		eqid	$⊢ \cdot_{T} = \cdot_{T}$
43	26 28 1 27 42	lmhmlin	$⊢ (G \in (S LMHom T) \land k \in {Base}_{Scalar (S)} \land F (x) \in B) \to G (k \cdot_{S} F (x)) = k \cdot_{T} G (F (x))$
44	41 21 25 43	syl3anc	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G (k \cdot_{S} F (x)) = k \cdot_{T} G (F (x))$
45		ffn	$⊢ F : I ⟶ B \to F Fn I$
46	45	ad2antrl	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to F Fn I$
47		fvco2	$⊢ (F Fn I \land x \in I) \to (G \circ F) (x) = G (F (x))$
48	46 23 47	syl2an	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to (G \circ F) (x) = G (F (x))$
49	48	oveq2d	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to k \cdot_{T} (G \circ F) (x) = k \cdot_{T} G (F (x))$
50	44 49	eqtr4d	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G (k \cdot_{S} F (x)) = k \cdot_{T} (G \circ F) (x)$
51		eqid	$⊢ LSpan (T) = LSpan (T)$
52	1 36 51	lmhmlsp	$⊢ (G \in (S LMHom T) \land F [I ∖ \{x\}] \subseteq B) \to G [LSpan (S) (F [I ∖ \{x\}])] = LSpan (T) (G [F [I ∖ \{x\}]])$
53	41 35 52	syl2anc	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G [LSpan (S) (F [I ∖ \{x\}])] = LSpan (T) (G [F [I ∖ \{x\}]])$
54		imaco	$⊢ (G \circ F) [I ∖ \{x\}] = G [F [I ∖ \{x\}]]$
55	54	fveq2i	$⊢ LSpan (T) ((G \circ F) [I ∖ \{x\}]) = LSpan (T) (G [F [I ∖ \{x\}]])$
56	53 55	eqtr4di	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to G [LSpan (S) (F [I ∖ \{x\}])] = LSpan (T) ((G \circ F) [I ∖ \{x\}])$
57	50 56	eleq12d	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to (G (k \cdot_{S} F (x)) \in G [LSpan (S) (F [I ∖ \{x\}])] \leftrightarrow k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
58	40 57	bitr3d	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to (k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
59	58	notbid	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land (x \in I \land k \in {Base}_{Scalar (S)})) \to (\neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
60	59	anassrs	$⊢ ((((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \land k \in {Base}_{Scalar (S)}) \to (\neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
61	17 60	sylan2	$⊢ ((((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \land k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\})) \to (\neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
62	61	ralbidva	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \to (\forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
63		eqid	$⊢ Scalar (T) = Scalar (T)$
64	26 63	lmhmsca	$⊢ G \in (S LMHom T) \to Scalar (T) = Scalar (S)$
65	64	fveq2d	$⊢ G \in (S LMHom T) \to {Base}_{Scalar (T)} = {Base}_{Scalar (S)}$
66	64	fveq2d	$⊢ G \in (S LMHom T) \to 0_{Scalar (T)} = 0_{Scalar (S)}$
67	66	sneqd	$⊢ G \in (S LMHom T) \to \{0_{Scalar (T)}\} = \{0_{Scalar (S)}\}$
68	65 67	difeq12d	$⊢ G \in (S LMHom T) \to {Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\} = {Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}$
69	68	ad3antrrr	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \to {Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\} = {Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}$
70	69	raleqdv	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \to (\forall k \in ({Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]) \leftrightarrow \forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
71	62 70	bitr4d	$⊢ (((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \land x \in I) \to (\forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \forall k \in ({Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
72	71	ralbidva	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to (\forall x \in I \forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]) \leftrightarrow \forall x \in I \forall k \in ({Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
73	19	ad2antrr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to S \in LMod$
74		simprr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to I \in V$
75		eqid	$⊢ 0_{Scalar (S)} = 0_{Scalar (S)}$
76	1 27 36 26 28 75	islindf2	$⊢ (S \in LMod \land I \in V \land F : I ⟶ B) \to (F LIndF S \leftrightarrow \forall x \in I \forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]))$
77	73 74 22 76	syl3anc	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to (F LIndF S \leftrightarrow \forall x \in I \forall k \in ({Base}_{Scalar (S)} ∖ \{0_{Scalar (S)}\}) \neg k \cdot_{S} F (x) \in LSpan (S) (F [I ∖ \{x\}]))$
78		lmhmlmod2	$⊢ G \in (S LMHom T) \to T \in LMod$
79	78	ad2antrr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to T \in LMod$
80	12	ad2ant2lr	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to (G \circ F) : I ⟶ C$
81		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
82		eqid	$⊢ 0_{Scalar (T)} = 0_{Scalar (T)}$
83	2 42 51 63 81 82	islindf2	$⊢ (T \in LMod \land I \in V \land (G \circ F) : I ⟶ C) \to ((G \circ F) LIndF T \leftrightarrow \forall x \in I \forall k \in ({Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
84	79 74 80 83	syl3anc	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to ((G \circ F) LIndF T \leftrightarrow \forall x \in I \forall k \in ({Base}_{Scalar (T)} ∖ \{0_{Scalar (T)}\}) \neg k \cdot_{T} (G \circ F) (x) \in LSpan (T) ((G \circ F) [I ∖ \{x\}]))$
85	72 77 84	3bitr4d	$⊢ ((G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \land (F : I ⟶ B \land I \in V)) \to (F LIndF S \leftrightarrow (G \circ F) LIndF T)$
86	85	exp32	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C) \to (F : I ⟶ B \to (I \in V \to (F LIndF S \leftrightarrow (G \circ F) LIndF T)))$
87	86	3impia	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (I \in V \to (F LIndF S \leftrightarrow (G \circ F) LIndF T))$
88	8 16 87	pm5.21ndd	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F : I ⟶ B) \to (F LIndF S \leftrightarrow (G \circ F) LIndF T)$

Metamath Proof Explorer

Theorem lindfmm

Proof