Theorem dimkerim 34329

Description: Given a linear map 𝐹 between vector spaces 𝑉 and 𝑈, the dimension of the vector space 𝑉 is the sum of the dimension of 𝐹 's kernel and the dimension of 𝐹's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dim‘𝐼) being the rank of 𝐹 (the dimension of its image), and (dim‘𝐾) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.)

Hypotheses

Ref	Expression
dimkerim.0	⊢ 0 = (0g‘𝑈)
dimkerim.k	⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 }))
dimkerim.i	⊢ 𝐼 = (𝑈 ↾s ran 𝐹)

Assertion

Ref	Expression
dimkerim	⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +e (dim‘𝐼)))

Proof of Theorem dimkerim

Dummy variables 𝑏 𝑢 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dimkerim.0	. . . . 5 ⊢ 0 = (0g‘𝑈)
2		dimkerim.k	. . . . 5 ⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 }))
3	1, 2	kerlmhm 34322	. . . 4 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4		eqid 2763	. . . . 5 ⊢ (LBasis‘𝐾) = (LBasis‘𝐾)
5	4	lbsex 21473	. . . 4 ⊢ (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
6	3, 5	syl 18	. . 3 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7		n0 4303	. . 3 ⊢ ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
8	6, 7	sylib 221	. 2 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9		simpllr 788	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10		vex 3458	. . . . . . 7 ⊢ 𝑏 ∈ V
11	10	difexi 5296	. . . . . 6 ⊢ (𝑏 ∖ 𝑤) ∈ V
12	11	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ V)
13		disjdif 4429	. . . . . 6 ⊢ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅)
15		hashunx 14557	. . . . 5 ⊢ ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏 ∖ 𝑤) ∈ V ∧ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +e (♯‘(𝑏 ∖ 𝑤))))
16	9, 12, 14, 15	syl3anc 1399	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +e (♯‘(𝑏 ∖ 𝑤))))
17		simp-4l 795	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LVec)
18		simpr 490	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ 𝑏)
19		undif 4441	. . . . . . 7 ⊢ (𝑤 ⊆ 𝑏 ↔ (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
20	18, 19	sylib 221	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
21		simplr 781	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘𝑉))
22	20, 21	eqeltrd 2864	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉))
23		eqid 2763	. . . . . 6 ⊢ (LBasis‘𝑉) = (LBasis‘𝑉)
24	23	dimval 34303	. . . . 5 ⊢ ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
25	17, 22, 24	syl2anc 596	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
26	3	ad3antrrr 743	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐾 ∈ LVec)
27	4	dimval 34303	. . . . . 6 ⊢ ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
28	26, 9, 27	syl2anc 596	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐾) = (♯‘𝑤))
29		dimkerim.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑈 ↾s ran 𝐹)
30	29	imlmhm 34323	. . . . . . . 8 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
31	30	ad3antrrr 743	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐼 ∈ LVec)
32		simp-4r 796	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33		lmhmlmod2 21337	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
34	32, 33	syl 18	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑈 ∈ LMod)
35		lmhmrnlss 21355	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
36	32, 35	syl 18	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37		df-ima 5668	. . . . . . . . . . 11 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
38		imassrn 6210	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹
39	38	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
40	37, 39	eqsstrrid 3952	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
41		lveclmod 21411	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod)
42	41	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LMod)
43	23	lbslinds 22169	. . . . . . . . . . . . . . 15 ⊢ (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
44	43, 21	sselid 3911	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45		difssd 4076	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ 𝑏)
46		lindsss 22160	. . . . . . . . . . . . . 14 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
47	42, 44, 45, 46	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
48		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑉) = (Base‘𝑉)
49	48	linds1 22146	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
50	47, 49	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
51		eqid 2763	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑉) = (LSubSp‘𝑉)
52		eqid 2763	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑉) = (LSpan‘𝑉)
53	48, 51, 52	lspcl 21281	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
54	42, 50, 53	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
55		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
56	51, 55	reslmhm 21357	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
57	32, 54, 56	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
58		eqid 2763	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
59	29, 58	reslmhm2b 21359	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼)))
60	59	biimpa 482	. . . . . . . . . 10 ⊢ (((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))
61	34, 36, 40, 57, 60	syl31anc 1401	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))
62		lmghm 21336	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
63	62	ad4antlr 746	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
64	48, 23	lbsss 21382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
65	21, 64	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ⊆ (Base‘𝑉))
66	45, 65	sstrd 3923	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
67	42, 66, 53	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
68	51	lsssubg 21262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
69	42, 67, 68	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
70	55	resghm 19475	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
71	63, 69, 70	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
72		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝑈) = (Base‘𝑈)
73	48, 72	lmhmf 21339	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
74	73	ad4antlr 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
75	74	ffnd 6732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 Fn (Base‘𝑉))
76	48, 52	lspssv 21288	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
77	42, 66, 76	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
78	75, 77	fnssresd 6685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
79		fniniseg 7083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )))
80	79	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ))
81	78, 80	sylan 592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ))
82	81	simpld 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
83	75	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉))
84	77	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
85	84, 82	sseldd 3914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
86	82	fvresd 6928	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = (𝐹‘𝑥))
87	81	simprd 501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )
88	86, 87	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝐹‘𝑥) = 0 )
89		fniniseg 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )))
90	89	biimpar 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 }))
91	83, 85, 88, 90	syl12anc 850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (◡𝐹 “ { 0 }))
92	82, 91	elind 4100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
93		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
94		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝐾) = (Base‘𝐾)
95		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (LSpan‘𝐾) = (LSpan‘𝐾)
96	94, 4, 95	lbssp 21384	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
97	93, 96	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
98	41	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
99		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 })
100	99, 1, 51	lmhmkerlss 21356	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
101	100	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
102	94, 4	lbsss 21382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
103	93, 102	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
104		cnvimass 6211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡𝐹 “ { 0 }) ⊆ dom 𝐹
105	104, 73	fssdm 6751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
106	2, 48	ressbas2 17445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((◡𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
107	105, 106	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
108	107	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
109	103, 108	sseqtrrd 3950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
110	2, 52, 95, 51	lsslsp 21320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤))
111	110	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
112	98, 101, 109, 111	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
113	97, 112, 108	3eqtr4d 2808	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
114	113	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
115	114	ineq2d 4120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
116		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘𝑉) = (0g‘𝑉)
117	23, 52, 116	lbsdiflsp0 34328	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
118	117	ad5ant145 1397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
119	115, 118	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) = {(0g‘𝑉)})
120	119	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) = {(0g‘𝑉)})
121	92, 120	eleqtrd 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ {(0g‘𝑉)})
122	121	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) → 𝑥 ∈ {(0g‘𝑉)}))
123	122	ssrdv 3919	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ⊆ {(0g‘𝑉)})
124	116, 48, 52	0ellsp 33995	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
125	42, 66, 124	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
126		fvexd 6923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V)
127	125	fvresd 6928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = (𝐹‘(0g‘𝑉)))
128	116, 1	ghmid 19465	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
129	62, 128	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
130	129	ad4antlr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹‘(0g‘𝑉)) = 0 )
131	127, 130	eqtrd 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 )
132		elsng 4598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ))
133	132	biimpar 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 })
134	126, 131, 133	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 })
135	78, 125, 134	elpreimad 7082	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
136	135	snssd 4747	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} ⊆ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
137	123, 136	eqssd 3930	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘𝑉)})
138		lmodgrp 21172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139		grpmnd 19180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
140	42, 138, 139	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ Mnd)
141	55, 48, 116	ress0g 18983	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 ∈ Mnd ∧ (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
142	140, 125, 77, 141	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
143	142	sneqd 4596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
144	137, 143	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
145		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
146		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
147	145, 72, 146, 1	kerf1ghm 19490	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1(Base‘𝑈) ↔ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}))
148	147	biimpar 483	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) ∧ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1(Base‘𝑈))
149	71, 144, 148	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1(Base‘𝑈))
150		eqidd 2764	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
151	55, 48	ressbas2 17445	. . . . . . . . . . . . . . . 16 ⊢ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
152	77, 151	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
153		eqidd 2764	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑈) = (Base‘𝑈))
154	150, 152, 153	f1eq123d 6838	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1(Base‘𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1(Base‘𝑈)))
155	149, 154	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1(Base‘𝑈))
156		f1ssr 6808	. . . . . . . . . . . . 13 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ran 𝐹)
157	155, 40, 156	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ran 𝐹)
158		f1f1orn 6858	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ran 𝐹 → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
159	157, 158	syl 18	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
160		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = 𝑦)
161	75	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉))
162		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤))
163	113	ad8antr 753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
164	162, 163	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (◡𝐹 “ { 0 }))
165		fniniseg 7083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (◡𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹‘𝑢) = 0 )))
166	165	simplbda 505	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑢) = 0 )
167	161, 164, 166	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑢) = 0 )
168	167	oveq1d 7458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = ( 0 (+g‘𝑈)(𝐹‘𝑣)))
169		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑥 = (𝑢(+g‘𝑉)𝑣))
170	169	fveq2d 6912	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝑉)𝑣)))
171	63	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
172	48, 52	lspss 21289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
173	42, 65, 18, 172	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
174	48, 23, 52	lbssp 21384	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
175	21, 174	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176	173, 175	sseqtrd 3949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
177	176	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
178	177	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
179	178, 162	sseldd 3914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉))
180	77	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
181	180	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
182		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
183	181, 182	sseldd 3914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑉) = (+g‘𝑉)
185		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑈) = (+g‘𝑈)
186	48, 184, 185	ghmlin 19464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
187	171, 179, 183, 186	syl3anc 1399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
188	170, 187	eqtr2d 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑥))
189		lmhmlvec2 34321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190	189	lvecgrpd 21413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
191	190	ad9antr 755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑈 ∈ Grp)
192	74	ad6antr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
193	192, 183	ffvelcdmd 7109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (Base‘𝑈))
194	72, 185, 1, 191, 193	grplidd 19209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ( 0 (+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑣))
195	168, 188, 194	3eqtr3d 2806	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘𝑣))
196	160, 195	eqtr3d 2800	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 = (𝐹‘𝑣))
197	161, 183, 182	fnfvimad 7263	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
198	196, 197	eqeltrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
199		simp-7l 801	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑉 ∈ LVec)
200		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
201	109	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
202	105	ad4antlr 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
203	201, 202	sstrd 3923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (Base‘𝑉))
204		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (LSSum‘𝑉) = (LSSum‘𝑉)
205	48, 52, 204	lsmsp2 21392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
206	42, 203, 66, 205	syl3anc 1399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
207	20	fveq2d 6912	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘𝑏))
208	206, 207, 175	3eqtrrd 2803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
209	208	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
210	200, 209	eleqtrd 2866	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
211	48, 184, 204	lsmelvalx 19884	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣)))
212	211	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) ∧ 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))
213	199, 177, 180, 210, 212	syl31anc 1401	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))
214	198, 213	r19.29vva 3226	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
215		fvelrnb 6968	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦))
216	215	biimpa 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
217	75, 216	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
218	214, 217	r19.29a 3174	. . . . . . . . . . . . . 14 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
219	39, 218	eqelssd 3934	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
220	37, 219	eqtr3id 2812	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
221	220	f1oeq3d 6843	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran 𝐹))
222	159, 221	mpbid 235	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran 𝐹)
223	42, 50, 76	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
224	223, 151	syl 18	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
225		frn 6739	. . . . . . . . . . . 12 ⊢ (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
226	29, 72	ressbas2 17445	. . . . . . . . . . . 12 ⊢ (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
227	32, 73, 225, 226	4syl 20	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 = (Base‘𝐼))
228	150, 224, 227	f1oeq123d 6840	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ontoran 𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1onto(Base‘𝐼)))
229	222, 228	mpbid 235	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1onto(Base‘𝐼))
230		eqid 2763	. . . . . . . . . 10 ⊢ (Base‘𝐼) = (Base‘𝐼)
231	145, 230	islmim 21367	. . . . . . . . 9 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))⟶1-1onto(Base‘𝐼)))
232	61, 229, 231	sylanbrc 595	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼))
233	48, 52	lspssid 21290	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
234	42, 50, 233	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
235	51, 55	lsslinds 22167	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)))
236	235	biimpar 483	. . . . . . . . . 10 ⊢ (((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
237	42, 67, 234, 47, 236	syl31anc 1401	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
238		eqid 2763	. . . . . . . . . . . . 13 ⊢ (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
239	55, 52, 238, 51	lsslsp 21320	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
240	239	eqcomd 2769	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
241	42, 54, 234, 240	syl3anc 1399	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
242	241, 224	eqtr3d 2800	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
243		eqid 2763	. . . . . . . . . 10 ⊢ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
244	145, 243, 238	islbs4 22168	. . . . . . . . 9 ⊢ ((𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ∧ ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))))
245	237, 242, 244	sylanbrc 595	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
246		eqid 2763	. . . . . . . . 9 ⊢ (LBasis‘𝐼) = (LBasis‘𝐼)
247	243, 246	lmimlbs 22172	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ∧ (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
248	232, 245, 247	syl2anc 596	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
249	246	dimval 34303	. . . . . . 7 ⊢ ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
250	31, 248, 249	syl2anc 596	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
251		f1imaeng 9069	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤))
252		hasheni 14519	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
253	251, 252	syl 18	. . . . . . 7 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))⟶1-1ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
254	157, 234, 47, 253	syl3anc 1399	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
255	250, 254	eqtrd 2798	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘(𝑏 ∖ 𝑤)))
256	28, 255	oveq12d 7461	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((dim‘𝐾) +e (dim‘𝐼)) = ((♯‘𝑤) +e (♯‘(𝑏 ∖ 𝑤))))
257	16, 25, 256	3eqtr4d 2808	. . 3 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = ((dim‘𝐾) +e (dim‘𝐼)))
258	4	lbslinds 22169	. . . . . 6 ⊢ (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
259	258, 93	sselid 3911	. . . . 5 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
260	51, 2	lsslinds 22167	. . . . . 6 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉)))
261	260	biimpa 482	. . . . 5 ⊢ (((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
262	98, 101, 109, 259, 261	syl31anc 1401	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
263	23	islinds4 22171	. . . . 5 ⊢ (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
264	263	ad2antrr 739	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
265	262, 264	mpbid 235	. . 3 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)
266	257, 265	r19.29a 3174	. 2 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +e (dim‘𝐼)))
267	8, 266	exlimddv 1970	1 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +e (dim‘𝐼)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588   class class class wbr 5106  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657   “ cima 5658   Fn wfn 6553  ⟶wf 6554  ⟶1-1wf1 6555  ⟶1-1ontowf1o 6557  ‘cfv 6558  (class class class)co 7443   ≈ cen 8998   +_e cxad 13266  ♯chash 14501  Basecbs 17416   ↾_s cress 17437  +_gcplusg 17457  0_gc0g 17639  Mndcmnd 18952  Grpcgrp 19173  SubGrpcsubg 19359   GrpHom cghm 19456  LSSumclsm 19878  LModclmod 21165  LSubSpclss 21236  LSpanclspn 21276   LMHom clmhm 21324   LMIso clmim 21325  LBasisclbs 21379  LVecclvec 21407  LIndSclinds 22141  dimcldim 34301

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669  ax-ac2 10568  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7717  df-rpss 7763  df-om 7902  df-1st 8025  df-2nd 8026  df-supp 8205  df-tpos 8271  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8745  df-map 8877  df-ixp 8954  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-fsupp 9382  df-sup 9461  df-oi 9531  df-dju 10009  df-card 10047  df-acn 10050  df-ac 10222  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-xnn0 12707  df-z 12721  df-dec 12842  df-uz 12993  df-xadd 13269  df-fz 13667  df-fzo 13816  df-seq 14172  df-hash 14502  df-struct 17354  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-mulr 17471  df-sca 17473  df-vsca 17474  df-ip 17475  df-tset 17476  df-ple 17477  df-ocomp 17478  df-ds 17479  df-hom 17481  df-cco 17482  df-0g 17641  df-gsum 17642  df-prds 17647  df-pws 17649  df-mre 17785  df-mrc 17786  df-mri 17787  df-acs 17788  df-proset 18497  df-drs 18498  df-poset 18516  df-ipo 18731  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-mhm 19007  df-submnd 19008  df-grp 19176  df-minusg 19177  df-sbg 19178  df-mulg 19307  df-subg 19362  df-ghm 19457  df-cntz 19561  df-lsm 19880  df-cmn 20026  df-abl 20027  df-mgp 20391  df-rng 20405  df-ur 20438  df-ring 20491  df-oppr 20597  df-dvdsr 20617  df-unit 20618  df-invr 20648  df-nzr 20793  df-subrg 20852  df-drng 21012  df-lmod 21167  df-lss 21237  df-lsp 21277  df-lmhm 21327  df-lmim 21328  df-lbs 21380  df-lvec 21408  df-sra 21478  df-rgmod 21479  df-dsmm 22068  df-frlm 22083  df-uvc 22119  df-lindf 22142  df-linds 22143  df-dim 34302

This theorem is used by:  qusdimsum  34330  lvecendof1f1o  34335