dimkerim

Description: Given a linear map F between vector spaces V and U , the dimension of the vector space V is the sum of the dimension of F 's kernel and the dimension of F 's image. Second part of theorem 5.3 in Lang p. 141 This can also be described as the Rank-nullity theorem, ( dimI ) being the rank of F (the dimension of its image), and ( dimK ) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023)

	Ref	Expression
Hypotheses	dimkerim.0	$⊢ \underset{˙}{0} = 0_{U}$
	dimkerim.k	$⊢ K = V ↾_{𝑠} F^{-1} [\{\underset{˙}{0}\}]$
	dimkerim.i	$⊢ I = U ↾_{𝑠} ran F$
Assertion	dimkerim	$⊢ (V \in LVec \land F \in (V LMHom U)) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$

Proof

Step	Hyp	Ref	Expression
1		dimkerim.0	$⊢ \underset{˙}{0} = 0_{U}$
2		dimkerim.k	$⊢ K = V ↾_{𝑠} F^{-1} [\{\underset{˙}{0}\}]$
3		dimkerim.i	$⊢ I = U ↾_{𝑠} ran F$
4	1 2	kerlmhm	$⊢ (V \in LVec \land F \in (V LMHom U)) \to K \in LVec$
5		eqid	$⊢ LBasis (K) = LBasis (K)$
6	5	lbsex	$⊢ K \in LVec \to LBasis (K) \neq \emptyset$
7	4 6	syl	$⊢ (V \in LVec \land F \in (V LMHom U)) \to LBasis (K) \neq \emptyset$
8		n0	$⊢ LBasis (K) \neq \emptyset \leftrightarrow \exists w w \in LBasis (K)$
9	7 8	sylib	$⊢ (V \in LVec \land F \in (V LMHom U)) \to \exists w w \in LBasis (K)$
10		simpllr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \in LBasis (K)$
11		vex	$⊢ b \in V$
12	11	difexi	$⊢ b ∖ w \in V$
13	12	a1i	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \in V$
14		disjdif	$⊢ w \cap (b ∖ w) = \emptyset$
15	14	a1i	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \cap (b ∖ w) = \emptyset$
16		hashunx	$⊢ (w \in LBasis (K) \land b ∖ w \in V \land w \cap (b ∖ w) = \emptyset) \to \|w \cup (b ∖ w)\| = \|w\| +_{𝑒} \|b ∖ w\|$
17	10 13 15 16	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \|w \cup (b ∖ w)\| = \|w\| +_{𝑒} \|b ∖ w\|$
18		simp-4l	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to V \in LVec$
19		simpr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \subseteq b$
20		undif	$⊢ w \subseteq b \leftrightarrow w \cup (b ∖ w) = b$
21	19 20	sylib	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \cup (b ∖ w) = b$
22		simplr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b \in LBasis (V)$
23	21 22	eqeltrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \cup (b ∖ w) \in LBasis (V)$
24		eqid	$⊢ LBasis (V) = LBasis (V)$
25	24	dimval	$⊢ (V \in LVec \land w \cup (b ∖ w) \in LBasis (V)) \to \dim (V) = \|w \cup (b ∖ w)\|$
26	18 23 25	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (V) = \|w \cup (b ∖ w)\|$
27	4	ad3antrrr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to K \in LVec$
28	5	dimval	$⊢ (K \in LVec \land w \in LBasis (K)) \to \dim (K) = \|w\|$
29	27 10 28	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (K) = \|w\|$
30	3	imlmhm	$⊢ (V \in LVec \land F \in (V LMHom U)) \to I \in LVec$
31	30	ad3antrrr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to I \in LVec$
32		simp-4r	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F \in (V LMHom U)$
33		lmhmlmod2	$⊢ F \in (V LMHom U) \to U \in LMod$
34	32 33	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to U \in LMod$
35		lmhmrnlss	$⊢ F \in (V LMHom U) \to ran F \in LSubSp (U)$
36	32 35	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ran F \in LSubSp (U)$
37		df-ima	$⊢ F [LSpan (V) (b ∖ w)] = ran ({F ↾}_{LSpan (V) (b ∖ w)})$
38		imassrn	$⊢ F [LSpan (V) (b ∖ w)] \subseteq ran F$
39	38	a1i	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F [LSpan (V) (b ∖ w)] \subseteq ran F$
40	37 39	eqsstrrid	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ran ({F ↾}_{LSpan (V) (b ∖ w)}) \subseteq ran F$
41		lveclmod	$⊢ V \in LVec \to V \in LMod$
42	41	ad4antr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to V \in LMod$
43	24	lbslinds	$⊢ LBasis (V) \subseteq LIndS (V)$
44	43 22	sselid	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b \in LIndS (V)$
45		difssd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \subseteq b$
46		lindsss	$⊢ (V \in LMod \land b \in LIndS (V) \land b ∖ w \subseteq b) \to b ∖ w \in LIndS (V)$
47	42 44 45 46	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \in LIndS (V)$
48		eqid	$⊢ {Base}_{V} = {Base}_{V}$
49	48	linds1	$⊢ b ∖ w \in LIndS (V) \to b ∖ w \subseteq {Base}_{V}$
50	47 49	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \subseteq {Base}_{V}$
51		eqid	$⊢ LSubSp (V) = LSubSp (V)$
52		eqid	$⊢ LSpan (V) = LSpan (V)$
53	48 51 52	lspcl	$⊢ (V \in LMod \land b ∖ w \subseteq {Base}_{V}) \to LSpan (V) (b ∖ w) \in LSubSp (V)$
54	42 50 53	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \in LSubSp (V)$
55		eqid	$⊢ V ↾_{𝑠} LSpan (V) (b ∖ w) = V ↾_{𝑠} LSpan (V) (b ∖ w)$
56	51 55	reslmhm	$⊢ (F \in (V LMHom U) \land LSpan (V) (b ∖ w) \in LSubSp (V)) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom U)$
57	32 54 56	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom U)$
58		eqid	$⊢ LSubSp (U) = LSubSp (U)$
59	3 58	reslmhm2b	$⊢ (U \in LMod \land ran F \in LSubSp (U) \land ran ({F ↾}_{LSpan (V) (b ∖ w)}) \subseteq ran F) \to ({F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom U) \leftrightarrow {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom I))$
60	59	biimpa	$⊢ ((U \in LMod \land ran F \in LSubSp (U) \land ran ({F ↾}_{LSpan (V) (b ∖ w)}) \subseteq ran F) \land {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom U)) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom I)$
61	34 36 40 57 60	syl31anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom I)$
62		lmghm	$⊢ F \in (V LMHom U) \to F \in (V GrpHom U)$
63	62	ad4antlr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F \in (V GrpHom U)$
64	48 24	lbsss	$⊢ b \in LBasis (V) \to b \subseteq {Base}_{V}$
65	22 64	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b \subseteq {Base}_{V}$
66	45 65	sstrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \subseteq {Base}_{V}$
67	42 66 53	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \in LSubSp (V)$
68	51	lsssubg	$⊢ (V \in LMod \land LSpan (V) (b ∖ w) \in LSubSp (V)) \to LSpan (V) (b ∖ w) \in SubGrp (V)$
69	42 67 68	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \in SubGrp (V)$
70	55	resghm	$⊢ (F \in (V GrpHom U) \land LSpan (V) (b ∖ w) \in SubGrp (V)) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) GrpHom U)$
71	63 69 70	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) GrpHom U)$
72		eqid	$⊢ {Base}_{U} = {Base}_{U}$
73	48 72	lmhmf	$⊢ F \in (V LMHom U) \to F : {Base}_{V} ⟶ {Base}_{U}$
74	73	ad4antlr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F : {Base}_{V} ⟶ {Base}_{U}$
75	74	ffnd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F Fn {Base}_{V}$
76	48 52	lspssv	$⊢ (V \in LMod \land b ∖ w \subseteq {Base}_{V}) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
77	42 66 76	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
78	75 77	fnssresd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) Fn LSpan (V) (b ∖ w)$
79		fniniseg	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)}) Fn LSpan (V) (b ∖ w) \to (x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in LSpan (V) (b ∖ w) \land ({F ↾}_{LSpan (V) (b ∖ w)}) (x) = \underset{˙}{0}))$
80	79	biimpa	$⊢ (({F ↾}_{LSpan (V) (b ∖ w)}) Fn LSpan (V) (b ∖ w) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to (x \in LSpan (V) (b ∖ w) \land ({F ↾}_{LSpan (V) (b ∖ w)}) (x) = \underset{˙}{0})$
81	78 80	sylan	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to (x \in LSpan (V) (b ∖ w) \land ({F ↾}_{LSpan (V) (b ∖ w)}) (x) = \underset{˙}{0})$
82	81	simpld	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to x \in LSpan (V) (b ∖ w)$
83	75	adantr	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to F Fn {Base}_{V}$
84	77	adantr	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
85	84 82	sseldd	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to x \in {Base}_{V}$
86	82	fvresd	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (x) = F (x)$
87	81	simprd	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (x) = \underset{˙}{0}$
88	86 87	eqtr3d	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to F (x) = \underset{˙}{0}$
89		fniniseg	$⊢ F Fn {Base}_{V} \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in {Base}_{V} \land F (x) = \underset{˙}{0}))$
90	89	biimpar	$⊢ (F Fn {Base}_{V} \land (x \in {Base}_{V} \land F (x) = \underset{˙}{0})) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
91	83 85 88 90	syl12anc	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
92	82 91	elind	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to x \in (LSpan (V) (b ∖ w) \cap F^{-1} [\{\underset{˙}{0}\}])$
93		simpr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LBasis (K)$
94		eqid	$⊢ {Base}_{K} = {Base}_{K}$
95		eqid	$⊢ LSpan (K) = LSpan (K)$
96	94 5 95	lbssp	$⊢ w \in LBasis (K) \to LSpan (K) (w) = {Base}_{K}$
97	93 96	syl	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to LSpan (K) (w) = {Base}_{K}$
98	41	ad2antrr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to V \in LMod$
99		eqid	$⊢ F^{-1} [\{\underset{˙}{0}\}] = F^{-1} [\{\underset{˙}{0}\}]$
100	99 1 51	lmhmkerlss	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V)$
101	100	ad2antlr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V)$
102	94 5	lbsss	$⊢ w \in LBasis (K) \to w \subseteq {Base}_{K}$
103	93 102	syl	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \subseteq {Base}_{K}$
104		cnvimass	$⊢ F^{-1} [\{\underset{˙}{0}\}] \subseteq dom F$
105	104 73	fssdm	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{V}$
106	2 48	ressbas2	$⊢ F^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{V} \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
107	105 106	syl	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
108	107	ad2antlr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
109	103 108	sseqtrrd	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \subseteq F^{-1} [\{\underset{˙}{0}\}]$
110	2 52 95 51	lsslsp	$⊢ (V \in LMod \land F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V) \land w \subseteq F^{-1} [\{\underset{˙}{0}\}]) \to LSpan (K) (w) = LSpan (V) (w)$
111	110	eqcomd	$⊢ (V \in LMod \land F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V) \land w \subseteq F^{-1} [\{\underset{˙}{0}\}]) \to LSpan (V) (w) = LSpan (K) (w)$
112	98 101 109 111	syl3anc	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to LSpan (V) (w) = LSpan (K) (w)$
113	97 112 108	3eqtr4d	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to LSpan (V) (w) = F^{-1} [\{\underset{˙}{0}\}]$
114	113	ad2antrr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (w) = F^{-1} [\{\underset{˙}{0}\}]$
115	114	ineq2d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \cap LSpan (V) (w) = LSpan (V) (b ∖ w) \cap F^{-1} [\{\underset{˙}{0}\}]$
116		eqid	$⊢ 0_{V} = 0_{V}$
117	24 52 116	lbsdiflsp0	$⊢ (V \in LVec \land b \in LBasis (V) \land w \subseteq b) \to LSpan (V) (b ∖ w) \cap LSpan (V) (w) = \{0_{V}\}$
118	117	ad5ant145	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \cap LSpan (V) (w) = \{0_{V}\}$
119	115 118	eqtr3d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \cap F^{-1} [\{\underset{˙}{0}\}] = \{0_{V}\}$
120	119	adantr	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to LSpan (V) (b ∖ w) \cap F^{-1} [\{\underset{˙}{0}\}] = \{0_{V}\}$
121	92 120	eleqtrd	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]) \to x \in \{0_{V}\}$
122	121	ex	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to (x \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] \to x \in \{0_{V}\})$
123	122	ssrdv	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] \subseteq \{0_{V}\}$
124	116 48 52	0ellsp	$⊢ (V \in LMod \land b ∖ w \subseteq {Base}_{V}) \to 0_{V} \in LSpan (V) (b ∖ w)$
125	42 66 124	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to 0_{V} \in LSpan (V) (b ∖ w)$
126		fvexd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in V$
127	125	fvresd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) = F (0_{V})$
128	116 1	ghmid	$⊢ F \in (V GrpHom U) \to F (0_{V}) = \underset{˙}{0}$
129	62 128	syl	$⊢ F \in (V LMHom U) \to F (0_{V}) = \underset{˙}{0}$
130	129	ad4antlr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F (0_{V}) = \underset{˙}{0}$
131	127 130	eqtrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) = \underset{˙}{0}$
132		elsng	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in V \to (({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in \{\underset{˙}{0}\} \leftrightarrow ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) = \underset{˙}{0})$
133	132	biimpar	$⊢ (({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in V \land ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) = \underset{˙}{0}) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in \{\underset{˙}{0}\}$
134	126 131 133	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) (0_{V}) \in \{\underset{˙}{0}\}$
135	78 125 134	elpreimad	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to 0_{V} \in {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]$
136	135	snssd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \{0_{V}\} \subseteq {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}]$
137	123 136	eqssd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] = \{0_{V}\}$
138		lmodgrp	$⊢ V \in LMod \to V \in Grp$
139		grpmnd	$⊢ V \in Grp \to V \in Mnd$
140	42 138 139	3syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to V \in Mnd$
141	55 48 116	ress0g	$⊢ (V \in Mnd \land 0_{V} \in LSpan (V) (b ∖ w) \land LSpan (V) (b ∖ w) \subseteq {Base}_{V}) \to 0_{V} = 0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
142	140 125 77 141	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to 0_{V} = 0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
143	142	sneqd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \{0_{V}\} = \{0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}\}$
144	137 143	eqtrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] = \{0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}\}$
145		eqid	$⊢ {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
146		eqid	$⊢ 0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} = 0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
147	145 72 146 1	kerf1ghm	$⊢ {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) GrpHom U) \to (({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1}{⟶} {Base}_{U} \leftrightarrow {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] = \{0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}\})$
148	147	biimpar	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) GrpHom U) \land {({F ↾}_{LSpan (V) (b ∖ w)})}^{-1} [\{\underset{˙}{0}\}] = \{0_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}\}) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1}{⟶} {Base}_{U}$
149	71 144 148	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1}{⟶} {Base}_{U}$
150		eqidd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {F ↾}_{LSpan (V) (b ∖ w)} = {F ↾}_{LSpan (V) (b ∖ w)}$
151	55 48	ressbas2	$⊢ LSpan (V) (b ∖ w) \subseteq {Base}_{V} \to LSpan (V) (b ∖ w) = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
152	77 151	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
153		eqidd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {Base}_{U} = {Base}_{U}$
154	150 152 153	f1eq123d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} {Base}_{U} \leftrightarrow ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1}{⟶} {Base}_{U})$
155	149 154	mpbird	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} {Base}_{U}$
156		f1ssr	$⊢ (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} {Base}_{U} \land ran ({F ↾}_{LSpan (V) (b ∖ w)}) \subseteq ran F) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} ran F$
157	155 40 156	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} ran F$
158		f1f1orn	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} ran F \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran ({F ↾}_{LSpan (V) (b ∖ w)})$
159	157 158	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran ({F ↾}_{LSpan (V) (b ∖ w)})$
160		simp-4r	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (x) = y$
161	75	ad6antr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F Fn {Base}_{V}$
162		simpllr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to u \in LSpan (V) (w)$
163	113	ad8antr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to LSpan (V) (w) = F^{-1} [\{\underset{˙}{0}\}]$
164	162 163	eleqtrd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to u \in F^{-1} [\{\underset{˙}{0}\}]$
165		fniniseg	$⊢ F Fn {Base}_{V} \to (u \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (u \in {Base}_{V} \land F (u) = \underset{˙}{0}))$
166	165	simplbda	$⊢ (F Fn {Base}_{V} \land u \in F^{-1} [\{\underset{˙}{0}\}]) \to F (u) = \underset{˙}{0}$
167	161 164 166	syl2anc	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (u) = \underset{˙}{0}$
168	167	oveq1d	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (u) +_{U} F (v) = \underset{˙}{0} +_{U} F (v)$
169		simpr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to x = u +_{V} v$
170	169	fveq2d	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (x) = F (u +_{V} v)$
171	63	ad6antr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F \in (V GrpHom U)$
172	48 52	lspss	$⊢ (V \in LMod \land b \subseteq {Base}_{V} \land w \subseteq b) \to LSpan (V) (w) \subseteq LSpan (V) (b)$
173	42 65 19 172	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (w) \subseteq LSpan (V) (b)$
174	48 24 52	lbssp	$⊢ b \in LBasis (V) \to LSpan (V) (b) = {Base}_{V}$
175	22 174	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b) = {Base}_{V}$
176	173 175	sseqtrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (w) \subseteq {Base}_{V}$
177	176	ad3antrrr	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to LSpan (V) (w) \subseteq {Base}_{V}$
178	177	ad3antrrr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to LSpan (V) (w) \subseteq {Base}_{V}$
179	178 162	sseldd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to u \in {Base}_{V}$
180	77	ad3antrrr	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
181	180	ad3antrrr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
182		simplr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to v \in LSpan (V) (b ∖ w)$
183	181 182	sseldd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to v \in {Base}_{V}$
184		eqid	$⊢ +_{V} = +_{V}$
185		eqid	$⊢ +_{U} = +_{U}$
186	48 184 185	ghmlin	$⊢ (F \in (V GrpHom U) \land u \in {Base}_{V} \land v \in {Base}_{V}) \to F (u +_{V} v) = F (u) +_{U} F (v)$
187	171 179 183 186	syl3anc	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (u +_{V} v) = F (u) +_{U} F (v)$
188	170 187	eqtr2d	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (u) +_{U} F (v) = F (x)$
189		lmhmlvec2	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in LVec$
190	189	lvecgrpd	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in Grp$
191	190	ad9antr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to U \in Grp$
192	74	ad6antr	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F : {Base}_{V} ⟶ {Base}_{U}$
193	192 183	ffvelcdmd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (v) \in {Base}_{U}$
194	72 185 1 191 193	grplidd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to \underset{˙}{0} +_{U} F (v) = F (v)$
195	168 188 194	3eqtr3d	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (x) = F (v)$
196	160 195	eqtr3d	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to y = F (v)$
197	161 183 182	fnfvimad	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to F (v) \in F [LSpan (V) (b ∖ w)]$
198	196 197	eqeltrd	$⊢ ((((((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \land u \in LSpan (V) (w)) \land v \in LSpan (V) (b ∖ w)) \land x = u +_{V} v) \to y \in F [LSpan (V) (b ∖ w)]$
199		simp-7l	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to V \in LVec$
200		simplr	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to x \in {Base}_{V}$
201	109	ad2antrr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \subseteq F^{-1} [\{\underset{˙}{0}\}]$
202	105	ad4antlr	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{V}$
203	201 202	sstrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to w \subseteq {Base}_{V}$
204		eqid	$⊢ LSSum (V) = LSSum (V)$
205	48 52 204	lsmsp2	$⊢ (V \in LMod \land w \subseteq {Base}_{V} \land b ∖ w \subseteq {Base}_{V}) \to LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w) = LSpan (V) (w \cup (b ∖ w))$
206	42 203 66 205	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w) = LSpan (V) (w \cup (b ∖ w))$
207	21	fveq2d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (w \cup (b ∖ w)) = LSpan (V) (b)$
208	206 207 175	3eqtrrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {Base}_{V} = LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w)$
209	208	ad3antrrr	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to {Base}_{V} = LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w)$
210	200 209	eleqtrd	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to x \in (LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w))$
211	48 184 204	lsmelvalx	$⊢ (V \in LVec \land LSpan (V) (w) \subseteq {Base}_{V} \land LSpan (V) (b ∖ w) \subseteq {Base}_{V}) \to (x \in (LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w)) \leftrightarrow \exists u \in LSpan (V) (w) \exists v \in LSpan (V) (b ∖ w) x = u +_{V} v)$
212	211	biimpa	$⊢ ((V \in LVec \land LSpan (V) (w) \subseteq {Base}_{V} \land LSpan (V) (b ∖ w) \subseteq {Base}_{V}) \land x \in (LSpan (V) (w) LSSum (V) LSpan (V) (b ∖ w))) \to \exists u \in LSpan (V) (w) \exists v \in LSpan (V) (b ∖ w) x = u +_{V} v$
213	199 177 180 210 212	syl31anc	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to \exists u \in LSpan (V) (w) \exists v \in LSpan (V) (b ∖ w) x = u +_{V} v$
214	198 213	r19.29vva	$⊢ (((((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \land x \in {Base}_{V}) \land F (x) = y) \to y \in F [LSpan (V) (b ∖ w)]$
215		fvelrnb	$⊢ F Fn {Base}_{V} \to (y \in ran F \leftrightarrow \exists x \in {Base}_{V} F (x) = y)$
216	215	biimpa	$⊢ (F Fn {Base}_{V} \land y \in ran F) \to \exists x \in {Base}_{V} F (x) = y$
217	75 216	sylan	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \to \exists x \in {Base}_{V} F (x) = y$
218	214 217	r19.29a	$⊢ (((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \land y \in ran F) \to y \in F [LSpan (V) (b ∖ w)]$
219	39 218	eqelssd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to F [LSpan (V) (b ∖ w)] = ran F$
220	37 219	eqtr3id	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ran ({F ↾}_{LSpan (V) (b ∖ w)}) = ran F$
221	220	f1oeq3d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran ({F ↾}_{LSpan (V) (b ∖ w)}) \leftrightarrow ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran F)$
222	159 221	mpbid	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran F$
223	42 50 76	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) \subseteq {Base}_{V}$
224	223 151	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
225		frn	$⊢ F : {Base}_{V} ⟶ {Base}_{U} \to ran F \subseteq {Base}_{U}$
226	3 72	ressbas2	$⊢ ran F \subseteq {Base}_{U} \to ran F = {Base}_{I}$
227	73 225 226	3syl	$⊢ F \in (V LMHom U) \to ran F = {Base}_{I}$
228	32 227	syl	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ran F = {Base}_{I}$
229	150 224 228	f1oeq123d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1 onto}{⟶} ran F \leftrightarrow ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1 onto}{⟶} {Base}_{I})$
230	222 229	mpbid	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1 onto}{⟶} {Base}_{I}$
231		eqid	$⊢ {Base}_{I} = {Base}_{I}$
232	145 231	islmim	$⊢ {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMIso I) \leftrightarrow ({F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMHom I) \land ({F ↾}_{LSpan (V) (b ∖ w)}) : {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))} \underset{1-1 onto}{⟶} {Base}_{I})$
233	61 230 232	sylanbrc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to {F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMIso I)$
234	48 52	lspssid	$⊢ (V \in LMod \land b ∖ w \subseteq {Base}_{V}) \to b ∖ w \subseteq LSpan (V) (b ∖ w)$
235	42 50 234	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \subseteq LSpan (V) (b ∖ w)$
236	51 55	lsslinds	$⊢ (V \in LMod \land LSpan (V) (b ∖ w) \in LSubSp (V) \land b ∖ w \subseteq LSpan (V) (b ∖ w)) \to (b ∖ w \in LIndS (V ↾_{𝑠} LSpan (V) (b ∖ w)) \leftrightarrow b ∖ w \in LIndS (V))$
237	236	biimpar	$⊢ ((V \in LMod \land LSpan (V) (b ∖ w) \in LSubSp (V) \land b ∖ w \subseteq LSpan (V) (b ∖ w)) \land b ∖ w \in LIndS (V)) \to b ∖ w \in LIndS (V ↾_{𝑠} LSpan (V) (b ∖ w))$
238	42 67 235 47 237	syl31anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \in LIndS (V ↾_{𝑠} LSpan (V) (b ∖ w))$
239		eqid	$⊢ LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) = LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w))$
240	55 52 239 51	lsslsp	$⊢ (V \in LMod \land LSpan (V) (b ∖ w) \in LSubSp (V) \land b ∖ w \subseteq LSpan (V) (b ∖ w)) \to LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) (b ∖ w) = LSpan (V) (b ∖ w)$
241	240	eqcomd	$⊢ (V \in LMod \land LSpan (V) (b ∖ w) \in LSubSp (V) \land b ∖ w \subseteq LSpan (V) (b ∖ w)) \to LSpan (V) (b ∖ w) = LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) (b ∖ w)$
242	42 54 235 241	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V) (b ∖ w) = LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) (b ∖ w)$
243	242 224	eqtr3d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) (b ∖ w) = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))}$
244		eqid	$⊢ LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w)) = LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w))$
245	145 244 239	islbs4	$⊢ b ∖ w \in LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w)) \leftrightarrow (b ∖ w \in LIndS (V ↾_{𝑠} LSpan (V) (b ∖ w)) \land LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) (b ∖ w) = {Base}_{(V ↾_{𝑠} LSpan (V) (b ∖ w))})$
246	238 243 245	sylanbrc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to b ∖ w \in LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w))$
247		eqid	$⊢ LBasis (I) = LBasis (I)$
248	244 247	lmimlbs	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)} \in ((V ↾_{𝑠} LSpan (V) (b ∖ w)) LMIso I) \land b ∖ w \in LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w))) \to ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \in LBasis (I)$
249	233 246 248	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \in LBasis (I)$
250	247	dimval	$⊢ (I \in LVec \land ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \in LBasis (I)) \to \dim (I) = \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\|$
251	31 249 250	syl2anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (I) = \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\|$
252		f1imaeng	$⊢ (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} ran F \land b ∖ w \subseteq LSpan (V) (b ∖ w) \land b ∖ w \in LIndS (V)) \to ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \approx (b ∖ w)$
253		hasheni	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \approx (b ∖ w) \to \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\| = \|b ∖ w\|$
254	252 253	syl	$⊢ (({F ↾}_{LSpan (V) (b ∖ w)}) : LSpan (V) (b ∖ w) \underset{1-1}{⟶} ran F \land b ∖ w \subseteq LSpan (V) (b ∖ w) \land b ∖ w \in LIndS (V)) \to \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\| = \|b ∖ w\|$
255	157 235 47 254	syl3anc	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\| = \|b ∖ w\|$
256	251 255	eqtrd	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (I) = \|b ∖ w\|$
257	29 256	oveq12d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (K) +_{𝑒} \dim (I) = \|w\| +_{𝑒} \|b ∖ w\|$
258	17 26 257	3eqtr4d	$⊢ ((((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \land b \in LBasis (V)) \land w \subseteq b) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$
259	5	lbslinds	$⊢ LBasis (K) \subseteq LIndS (K)$
260	259 93	sselid	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LIndS (K)$
261	51 2	lsslinds	$⊢ (V \in LMod \land F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V) \land w \subseteq F^{-1} [\{\underset{˙}{0}\}]) \to (w \in LIndS (K) \leftrightarrow w \in LIndS (V))$
262	261	biimpa	$⊢ ((V \in LMod \land F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V) \land w \subseteq F^{-1} [\{\underset{˙}{0}\}]) \land w \in LIndS (K)) \to w \in LIndS (V)$
263	98 101 109 260 262	syl31anc	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LIndS (V)$
264	24	islinds4	$⊢ V \in LVec \to (w \in LIndS (V) \leftrightarrow \exists b \in LBasis (V) w \subseteq b)$
265	264	ad2antrr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to (w \in LIndS (V) \leftrightarrow \exists b \in LBasis (V) w \subseteq b)$
266	263 265	mpbid	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to \exists b \in LBasis (V) w \subseteq b$
267	258 266	r19.29a	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$
268	9 267	exlimddv	$⊢ (V \in LVec \land F \in (V LMHom U)) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$

Metamath Proof Explorer

Theorem dimkerim

Proof