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	sseldi	$⊢ ((((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		fnssres	$⊢ (F Fn {Base}_{V} \land LSpan (V) (b ∖ w) \subseteq {Base}_{V}) \to ({F ↾}_{LSpan (V) (b ∖ w)}) Fn LSpan (V) (b ∖ w)$
79	75 77 78	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)}) Fn LSpan (V) (b ∖ w)$
80		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}))$
81	80	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})$
82	79 81	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})$
83	82	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)$
84	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}$
85	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}$
86	85 83	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}$
87	83	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)$
88	82	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}$
89	87 88	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}$
90		fniniseg	$⊢ F Fn {Base}_{V} \to (x \in F^{-1} [\{\underset{˙}{0}\}] \leftrightarrow (x \in {Base}_{V} \land F (x) = \underset{˙}{0}))$
91	90	biimpar	$⊢ (F Fn {Base}_{V} \land (x \in {Base}_{V} \land F (x) = \underset{˙}{0})) \to x \in F^{-1} [\{\underset{˙}{0}\}]$
92	84 86 89 91	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}\}]$
93	83 92	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}\}])$
94		simpr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LBasis (K)$
95		eqid	$⊢ {Base}_{K} = {Base}_{K}$
96		eqid	$⊢ LSpan (K) = LSpan (K)$
97	95 5 96	lbssp	$⊢ w \in LBasis (K) \to LSpan (K) (w) = {Base}_{K}$
98	94 97	syl	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to LSpan (K) (w) = {Base}_{K}$
99	41	ad2antrr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to V \in LMod$
100		eqid	$⊢ F^{-1} [\{\underset{˙}{0}\}] = F^{-1} [\{\underset{˙}{0}\}]$
101	100 1 51	lmhmkerlss	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V)$
102	101	ad2antlr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to F^{-1} [\{\underset{˙}{0}\}] \in LSubSp (V)$
103	95 5	lbsss	$⊢ w \in LBasis (K) \to w \subseteq {Base}_{K}$
104	94 103	syl	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \subseteq {Base}_{K}$
105		cnvimass	$⊢ F^{-1} [\{\underset{˙}{0}\}] \subseteq dom F$
106	105 73	fssdm	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{V}$
107	2 48	ressbas2	$⊢ F^{-1} [\{\underset{˙}{0}\}] \subseteq {Base}_{V} \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
108	106 107	syl	$⊢ F \in (V LMHom U) \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
109	108	ad2antlr	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to F^{-1} [\{\underset{˙}{0}\}] = {Base}_{K}$
110	104 109	sseqtrrd	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \subseteq F^{-1} [\{\underset{˙}{0}\}]$
111	2 52 96 51	lsslsp	$⊢ (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	99 102 110 111	syl3anc	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to LSpan (V) (w) = LSpan (K) (w)$
113	98 112 109	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	93 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	79 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		lveclmod	$⊢ U \in LVec \to U \in LMod$
191		lmodgrp	$⊢ U \in LMod \to U \in Grp$
192	189 190 191	3syl	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in Grp$
193	192	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$
194	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}$
195	194 183	ffvelrnd	$⊢ ((((((((((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}$
196	72 185 1	grplid	$⊢ (U \in Grp \land F (v) \in {Base}_{U}) \to \underset{˙}{0} +_{U} F (v) = F (v)$
197	193 195 196	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 \underset{˙}{0} +_{U} F (v) = F (v)$
198	168 188 197	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)$
199	160 198	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)$
200	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)]$
201	199 200	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)]$
202		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$
203		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}$
204	110	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}\}]$
205	106	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}$
206	204 205	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}$
207		eqid	$⊢ LSSum (V) = LSSum (V)$
208	48 52 207	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))$
209	42 206 66 208	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))$
210	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)$
211	209 210 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)$
212	211	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)$
213	203 212	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))$
214	48 184 207	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)$
215	214	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$
216	202 177 180 213 215	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$
217	201 216	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)]$
218		fvelrnb	$⊢ F Fn {Base}_{V} \to (y \in ran F \leftrightarrow \exists x \in {Base}_{V} F (x) = y)$
219	218	biimpa	$⊢ (F Fn {Base}_{V} \land y \in ran F) \to \exists x \in {Base}_{V} F (x) = y$
220	75 219	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$
221	217 220	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)]$
222	39 221	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$
223	37 222	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$
224	223	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)$
225	159 224	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$
226	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}$
227	226 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))}$
228		frn	$⊢ F : {Base}_{V} ⟶ {Base}_{U} \to ran F \subseteq {Base}_{U}$
229	3 72	ressbas2	$⊢ ran F \subseteq {Base}_{U} \to ran F = {Base}_{I}$
230	73 228 229	3syl	$⊢ F \in (V LMHom U) \to ran F = {Base}_{I}$
231	32 230	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}$
232	150 227 231	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})$
233	225 232	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}$
234		eqid	$⊢ {Base}_{I} = {Base}_{I}$
235	145 234	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})$
236	61 233 235	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)$
237	48 52	lspssid	$⊢ (V \in LMod \land b ∖ w \subseteq {Base}_{V}) \to b ∖ w \subseteq LSpan (V) (b ∖ w)$
238	42 50 237	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)$
239	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))$
240	239	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))$
241	42 67 238 47 240	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))$
242		eqid	$⊢ LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w)) = LSpan (V ↾_{𝑠} LSpan (V) (b ∖ w))$
243	55 52 242 51	lsslsp	$⊢ (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)$
244	42 54 238 243	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)$
245	244 227	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))}$
246		eqid	$⊢ LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w)) = LBasis (V ↾_{𝑠} LSpan (V) (b ∖ w))$
247	145 246 242	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))})$
248	241 245 247	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))$
249		eqid	$⊢ LBasis (I) = LBasis (I)$
250	246 249	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)$
251	236 248 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 ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \in LBasis (I)$
252	249	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]\|$
253	31 251 252	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]\|$
254		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)$
255		hasheni	$⊢ ({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w] \approx (b ∖ w) \to \|({F ↾}_{LSpan (V) (b ∖ w)}) [b ∖ w]\| = \|b ∖ w\|$
256	254 255	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\|$
257	157 238 47 256	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\|$
258	253 257	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\|$
259	29 258	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\|$
260	17 26 259	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)$
261	5	lbslinds	$⊢ LBasis (K) \subseteq LIndS (K)$
262	261 94	sseldi	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LIndS (K)$
263	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))$
264	263	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)$
265	99 102 110 262 264	syl31anc	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to w \in LIndS (V)$
266	24	islinds4	$⊢ V \in LVec \to (w \in LIndS (V) \leftrightarrow \exists b \in LBasis (V) w \subseteq b)$
267	266	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)$
268	265 267	mpbid	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to \exists b \in LBasis (V) w \subseteq b$
269	260 268	r19.29a	$⊢ ((V \in LVec \land F \in (V LMHom U)) \land w \in LBasis (K)) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$
270	9 269	exlimddv	$⊢ (V \in LVec \land F \in (V LMHom U)) \to \dim (V) = \dim (K) +_{𝑒} \dim (I)$

Metamath Proof Explorer

Theorem dimkerim

Proof