f1lindf

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

		Ref	Expression
	Assertion	f1lindf	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to (F \circ G) LIndF W$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{W} = {Base}_{W}$
2	1	lindff	$⊢ (F LIndF W \land W \in LMod) \to F : dom F ⟶ {Base}_{W}$
3	2	ancoms	$⊢ (W \in LMod \land F LIndF W) \to F : dom F ⟶ {Base}_{W}$
4	3	3adant3	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to F : dom F ⟶ {Base}_{W}$
5		f1f	$⊢ G : K \underset{1-1}{⟶} dom F \to G : K ⟶ dom F$
6	5	3ad2ant3	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G : K ⟶ dom F$
7		fco	$⊢ (F : dom F ⟶ {Base}_{W} \land G : K ⟶ dom F) \to (F \circ G) : K ⟶ {Base}_{W}$
8	4 6 7	syl2anc	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to (F \circ G) : K ⟶ {Base}_{W}$
9	8	ffdmd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to (F \circ G) : dom (F \circ G) ⟶ {Base}_{W}$
10		simpl2	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to F LIndF W$
11	6	adantr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to G : K ⟶ dom F$
12	8	fdmd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to dom (F \circ G) = K$
13	12	eleq2d	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to (x \in dom (F \circ G) \leftrightarrow x \in K)$
14	13	biimpa	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to x \in K$
15	11 14	ffvelcdmd	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to G (x) \in dom F$
16	15	adantrr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to G (x) \in dom F$
17		eldifi	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \in {Base}_{Scalar (W)}$
18	17	ad2antll	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to k \in {Base}_{Scalar (W)}$
19		eldifsni	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \neq 0_{Scalar (W)}$
20	19	ad2antll	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to k \neq 0_{Scalar (W)}$
21		eqid	$⊢ \cdot_{W} = \cdot_{W}$
22		eqid	$⊢ LSpan (W) = LSpan (W)$
23		eqid	$⊢ Scalar (W) = Scalar (W)$
24		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
25		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
26	21 22 23 24 25	lindfind	$⊢ ((F LIndF W \land G (x) \in dom F) \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})) \to \neg k \cdot_{W} F (G (x)) \in LSpan (W) (F [dom F ∖ \{G (x)\}])$
27	10 16 18 20 26	syl22anc	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg k \cdot_{W} F (G (x)) \in LSpan (W) (F [dom F ∖ \{G (x)\}])$
28		f1fn	$⊢ G : K \underset{1-1}{⟶} dom F \to G Fn K$
29	28	3ad2ant3	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G Fn K$
30	29	adantr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to G Fn K$
31		fvco2	$⊢ (G Fn K \land x \in K) \to (F \circ G) (x) = F (G (x))$
32	30 14 31	syl2anc	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to (F \circ G) (x) = F (G (x))$
33	32	oveq2d	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to k \cdot_{W} (F \circ G) (x) = k \cdot_{W} F (G (x))$
34	33	eleq1d	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to (k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \leftrightarrow k \cdot_{W} F (G (x)) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]))$
35		simpl1	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to W \in LMod$
36		imassrn	$⊢ F [dom F ∖ \{G (x)\}] \subseteq ran F$
37	4	frnd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to ran F \subseteq {Base}_{W}$
38	36 37	sstrid	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to F [dom F ∖ \{G (x)\}] \subseteq {Base}_{W}$
39	38	adantr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to F [dom F ∖ \{G (x)\}] \subseteq {Base}_{W}$
40		imaco	$⊢ (F \circ G) [dom (F \circ G) ∖ \{x\}] = F [G [dom (F \circ G) ∖ \{x\}]]$
41	12	difeq1d	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to dom (F \circ G) ∖ \{x\} = K ∖ \{x\}$
42	41	imaeq2d	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G [dom (F \circ G) ∖ \{x\}] = G [K ∖ \{x\}]$
43		df-f1	$⊢ G : K \underset{1-1}{⟶} dom F \leftrightarrow (G : K ⟶ dom F \land Fun G^{-1})$
44	43	simprbi	$⊢ G : K \underset{1-1}{⟶} dom F \to Fun G^{-1}$
45	44	3ad2ant3	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to Fun G^{-1}$
46		imadif	$⊢ Fun G^{-1} \to G [K ∖ \{x\}] = G [K] ∖ G [\{x\}]$
47	45 46	syl	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G [K ∖ \{x\}] = G [K] ∖ G [\{x\}]$
48	42 47	eqtrd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G [dom (F \circ G) ∖ \{x\}] = G [K] ∖ G [\{x\}]$
49	48	adantr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [dom (F \circ G) ∖ \{x\}] = G [K] ∖ G [\{x\}]$
50		fnsnfv	$⊢ (G Fn K \land x \in K) \to \{G (x)\} = G [\{x\}]$
51	29 50	sylan	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to \{G (x)\} = G [\{x\}]$
52	51	difeq2d	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [K] ∖ \{G (x)\} = G [K] ∖ G [\{x\}]$
53		imassrn	$⊢ G [K] \subseteq ran G$
54	6	adantr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G : K ⟶ dom F$
55	54	frnd	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to ran G \subseteq dom F$
56	53 55	sstrid	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [K] \subseteq dom F$
57	56	ssdifd	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [K] ∖ \{G (x)\} \subseteq dom F ∖ \{G (x)\}$
58	52 57	eqsstrrd	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [K] ∖ G [\{x\}] \subseteq dom F ∖ \{G (x)\}$
59	49 58	eqsstrd	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to G [dom (F \circ G) ∖ \{x\}] \subseteq dom F ∖ \{G (x)\}$
60		imass2	$⊢ G [dom (F \circ G) ∖ \{x\}] \subseteq dom F ∖ \{G (x)\} \to F [G [dom (F \circ G) ∖ \{x\}]] \subseteq F [dom F ∖ \{G (x)\}]$
61	59 60	syl	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to F [G [dom (F \circ G) ∖ \{x\}]] \subseteq F [dom F ∖ \{G (x)\}]$
62	40 61	eqsstrid	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to (F \circ G) [dom (F \circ G) ∖ \{x\}] \subseteq F [dom F ∖ \{G (x)\}]$
63	1 22	lspss	$⊢ (W \in LMod \land F [dom F ∖ \{G (x)\}] \subseteq {Base}_{W} \land (F \circ G) [dom (F \circ G) ∖ \{x\}] \subseteq F [dom F ∖ \{G (x)\}]) \to LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \subseteq LSpan (W) (F [dom F ∖ \{G (x)\}])$
64	35 39 62 63	syl3anc	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in K) \to LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \subseteq LSpan (W) (F [dom F ∖ \{G (x)\}])$
65	14 64	syldan	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \subseteq LSpan (W) (F [dom F ∖ \{G (x)\}])$
66	65	sseld	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to (k \cdot_{W} F (G (x)) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \to k \cdot_{W} F (G (x)) \in LSpan (W) (F [dom F ∖ \{G (x)\}]))$
67	34 66	sylbid	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land x \in dom (F \circ G)) \to (k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \to k \cdot_{W} F (G (x)) \in LSpan (W) (F [dom F ∖ \{G (x)\}]))$
68	67	adantrr	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}]) \to k \cdot_{W} F (G (x)) \in LSpan (W) (F [dom F ∖ \{G (x)\}]))$
69	27 68	mtod	$⊢ ((W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \land (x \in dom (F \circ G) \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}])$
70	69	ralrimivva	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to \forall x \in dom (F \circ G) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}])$
71		simp1	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to W \in LMod$
72		rellindf	$⊢ Rel LIndF$
73	72	brrelex1i	$⊢ F LIndF W \to F \in V$
74	73	3ad2ant2	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to F \in V$
75		simp3	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G : K \underset{1-1}{⟶} dom F$
76	74	dmexd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to dom F \in V$
77		f1dmex	$⊢ (G : K \underset{1-1}{⟶} dom F \land dom F \in V) \to K \in V$
78	75 76 77	syl2anc	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to K \in V$
79	6 78	fexd	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to G \in V$
80		coexg	$⊢ (F \in V \land G \in V) \to F \circ G \in V$
81	74 79 80	syl2anc	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to F \circ G \in V$
82	1 21 22 23 25 24	islindf	$⊢ (W \in LMod \land F \circ G \in V) \to ((F \circ G) LIndF W \leftrightarrow ((F \circ G) : dom (F \circ G) ⟶ {Base}_{W} \land \forall x \in dom (F \circ G) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}])))$
83	71 81 82	syl2anc	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to ((F \circ G) LIndF W \leftrightarrow ((F \circ G) : dom (F \circ G) ⟶ {Base}_{W} \land \forall x \in dom (F \circ G) \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} (F \circ G) (x) \in LSpan (W) ((F \circ G) [dom (F \circ G) ∖ \{x\}])))$
84	9 70 83	mpbir2and	$⊢ (W \in LMod \land F LIndF W \land G : K \underset{1-1}{⟶} dom F) \to (F \circ G) LIndF W$

Metamath Proof Explorer

Theorem f1lindf

Proof