Theorem dimkerim 33640

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‘𝐾) +𝑒 (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 33633	. . . 4 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4		eqid 2740	. . . . 5 ⊢ (LBasis‘𝐾) = (LBasis‘𝐾)
5	4	lbsex 21190	. . . 4 ⊢ (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
6	3, 5	syl 17	. . 3 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7		n0 4376	. . 3 ⊢ ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
8	6, 7	sylib 218	. 2 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9		simpllr 775	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10		vex 3492	. . . . . . 7 ⊢ 𝑏 ∈ V
11	10	difexi 5348	. . . . . 6 ⊢ (𝑏 ∖ 𝑤) ∈ V
12	11	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ V)
13		disjdif 4495	. . . . . 6 ⊢ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅)
15		hashunx 14435	. . . . 5 ⊢ ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏 ∖ 𝑤) ∈ V ∧ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
16	9, 12, 14, 15	syl3anc 1371	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
17		simp-4l 782	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LVec)
18		simpr 484	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ 𝑏)
19		undif 4505	. . . . . . 7 ⊢ (𝑤 ⊆ 𝑏 ↔ (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
20	18, 19	sylib 218	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
21		simplr 768	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘𝑉))
22	20, 21	eqeltrd 2844	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉))
23		eqid 2740	. . . . . 6 ⊢ (LBasis‘𝑉) = (LBasis‘𝑉)
24	23	dimval 33613	. . . . 5 ⊢ ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
25	17, 22, 24	syl2anc 583	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
26	3	ad3antrrr 729	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐾 ∈ LVec)
27	4	dimval 33613	. . . . . 6 ⊢ ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
28	26, 9, 27	syl2anc 583	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐾) = (♯‘𝑤))
29		dimkerim.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑈 ↾s ran 𝐹)
30	29	imlmhm 33634	. . . . . . . 8 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
31	30	ad3antrrr 729	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐼 ∈ LVec)
32		simp-4r 783	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33		lmhmlmod2 21054	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑈 ∈ LMod)
35		lmhmrnlss 21072	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
36	32, 35	syl 17	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37		df-ima 5713	. . . . . . . . . . 11 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
38		imassrn 6100	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹
39	38	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
40	37, 39	eqsstrrid 4058	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
41		lveclmod 21128	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod)
42	41	ad4antr 731	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LMod)
43	23	lbslinds 21876	. . . . . . . . . . . . . . 15 ⊢ (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
44	43, 21	sselid 4006	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45		difssd 4160	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ 𝑏)
46		lindsss 21867	. . . . . . . . . . . . . 14 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
47	42, 44, 45, 46	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
48		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑉) = (Base‘𝑉)
49	48	linds1 21853	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
50	47, 49	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
51		eqid 2740	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑉) = (LSubSp‘𝑉)
52		eqid 2740	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑉) = (LSpan‘𝑉)
53	48, 51, 52	lspcl 20997	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
54	42, 50, 53	syl2anc 583	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
55		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
56	51, 55	reslmhm 21074	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
57	32, 54, 56	syl2anc 583	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
58		eqid 2740	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
59	29, 58	reslmhm2b 21076	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼)))
60	59	biimpa 476	. . . . . . . . . 10 ⊢ (((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))
61	34, 36, 40, 57, 60	syl31anc 1373	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))
62		lmghm 21053	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
63	62	ad4antlr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
64	48, 23	lbsss 21099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
65	21, 64	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ⊆ (Base‘𝑉))
66	45, 65	sstrd 4019	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
67	42, 66, 53	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
68	51	lsssubg 20978	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
69	42, 67, 68	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
70	55	resghm 19272	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
71	63, 69, 70	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
72		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝑈) = (Base‘𝑈)
73	48, 72	lmhmf 21056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
74	73	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
75	74	ffnd 6748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 Fn (Base‘𝑉))
76	48, 52	lspssv 21004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
77	42, 66, 76	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
78	75, 77	fnssresd 6704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
79		fniniseg 7093	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )))
80	79	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ))
81	78, 80	sylan 579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ))
82	81	simpld 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
83	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉))
84	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
85	84, 82	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
86	82	fvresd 6940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = (𝐹‘𝑥))
87	81	simprd 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )
88	86, 87	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝐹‘𝑥) = 0 )
89		fniniseg 7093	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )))
90	89	biimpar 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 }))
91	83, 85, 88, 90	syl12anc 836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (◡𝐹 “ { 0 }))
92	82, 91	elind 4223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
93		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
94		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝐾) = (Base‘𝐾)
95		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (LSpan‘𝐾) = (LSpan‘𝐾)
96	94, 4, 95	lbssp 21101	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
97	93, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
98	41	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
99		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 })
100	99, 1, 51	lmhmkerlss 21073	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
101	100	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
102	94, 4	lbsss 21099	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
103	93, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
104		cnvimass 6111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡𝐹 “ { 0 }) ⊆ dom 𝐹
105	104, 73	fssdm 6766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
106	2, 48	ressbas2 17296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((◡𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
108	107	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
109	103, 108	sseqtrrd 4050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
110	2, 52, 95, 51	lsslsp 21036	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤))
111	110	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
112	98, 101, 109, 111	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
113	97, 112, 108	3eqtr4d 2790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
114	113	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
115	114	ineq2d 4241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
116		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘𝑉) = (0g‘𝑉)
117	23, 52, 116	lbsdiflsp0 33639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
118	117	ad5ant145 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
119	115, 118	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) = {(0g‘𝑉)})
120	119	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) = {(0g‘𝑉)})
121	92, 120	eleqtrd 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ {(0g‘𝑉)})
122	121	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) → 𝑥 ∈ {(0g‘𝑉)}))
123	122	ssrdv 4014	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ⊆ {(0g‘𝑉)})
124	116, 48, 52	0ellsp 33362	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
125	42, 66, 124	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
126		fvexd 6935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V)
127	125	fvresd 6940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = (𝐹‘(0g‘𝑉)))
128	116, 1	ghmid 19262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
129	62, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
130	129	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹‘(0g‘𝑉)) = 0 )
131	127, 130	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 )
132		elsng 4662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ))
133	132	biimpar 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 })
134	126, 131, 133	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 })
135	78, 125, 134	elpreimad 7092	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
136	135	snssd 4834	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} ⊆ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
137	123, 136	eqssd 4026	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘𝑉)})
138		lmodgrp 20887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139		grpmnd 18980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
140	42, 138, 139	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ Mnd)
141	55, 48, 116	ress0g 18800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 ∈ Mnd ∧ (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
142	140, 125, 77, 141	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
143	142	sneqd 4660	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
144	137, 143	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
145		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
146		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
147	145, 72, 146, 1	kerf1ghm 19287	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈) ↔ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}))
148	147	biimpar 477	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) ∧ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈))
149	71, 144, 148	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈))
150		eqidd 2741	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
151	55, 48	ressbas2 17296	. . . . . . . . . . . . . . . 16 ⊢ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
152	77, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
153		eqidd 2741	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑈) = (Base‘𝑈))
154	150, 152, 153	f1eq123d 6854	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈)))
155	149, 154	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈))
156		f1ssr 6823	. . . . . . . . . . . . 13 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹)
157	155, 40, 156	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹)
158		f1f1orn 6873	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
159	157, 158	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
160		simp-4r 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = 𝑦)
161	75	ad6antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉))
162		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤))
163	113	ad8antr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
164	162, 163	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (◡𝐹 “ { 0 }))
165		fniniseg 7093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (◡𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹‘𝑢) = 0 )))
166	165	simplbda 499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑢) = 0 )
167	161, 164, 166	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑢) = 0 )
168	167	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = ( 0 (+g‘𝑈)(𝐹‘𝑣)))
169		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑥 = (𝑢(+g‘𝑉)𝑣))
170	169	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝑉)𝑣)))
171	63	ad6antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
172	48, 52	lspss 21005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
173	42, 65, 18, 172	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
174	48, 23, 52	lbssp 21101	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
175	21, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176	173, 175	sseqtrd 4049	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
177	176	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
178	177	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
179	178, 162	sseldd 4009	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉))
180	77	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
181	180	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
182		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
183	181, 182	sseldd 4009	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑉) = (+g‘𝑉)
185		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑈) = (+g‘𝑈)
186	48, 184, 185	ghmlin 19261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
187	171, 179, 183, 186	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
188	170, 187	eqtr2d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑥))
189		lmhmlvec2 33632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190	189	lvecgrpd 21130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
191	190	ad9antr 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑈 ∈ Grp)
192	74	ad6antr 735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
193	192, 183	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (Base‘𝑈))
194	72, 185, 1, 191, 193	grplidd 19009	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ( 0 (+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑣))
195	168, 188, 194	3eqtr3d 2788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘𝑣))
196	160, 195	eqtr3d 2782	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 = (𝐹‘𝑣))
197	161, 183, 182	fnfvimad 7271	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
198	196, 197	eqeltrd 2844	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
199		simp-7l 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑉 ∈ LVec)
200		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
201	109	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
202	105	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
203	201, 202	sstrd 4019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (Base‘𝑉))
204		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (LSSum‘𝑉) = (LSSum‘𝑉)
205	48, 52, 204	lsmsp2 21109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
206	42, 203, 66, 205	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
207	20	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘𝑏))
208	206, 207, 175	3eqtrrd 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
209	208	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
210	200, 209	eleqtrd 2846	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
211	48, 184, 204	lsmelvalx 19682	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣)))
212	211	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) ∧ 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))
213	199, 177, 180, 210, 212	syl31anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))
214	198, 213	r19.29vva 3222	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
215		fvelrnb 6982	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦))
216	215	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
217	75, 216	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
218	214, 217	r19.29a 3168	. . . . . . . . . . . . . 14 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
219	39, 218	eqelssd 4030	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
220	37, 219	eqtr3id 2794	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
221	220	f1oeq3d 6859	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran 𝐹))
222	159, 221	mpbid 232	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran 𝐹)
223	42, 50, 76	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
224	223, 151	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
225		frn 6754	. . . . . . . . . . . 12 ⊢ (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
226	29, 72	ressbas2 17296	. . . . . . . . . . . 12 ⊢ (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
227	32, 73, 225, 226	4syl 19	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 = (Base‘𝐼))
228	150, 224, 227	f1oeq123d 6856	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼)))
229	222, 228	mpbid 232	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼))
230		eqid 2740	. . . . . . . . . 10 ⊢ (Base‘𝐼) = (Base‘𝐼)
231	145, 230	islmim 21084	. . . . . . . . 9 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼)))
232	61, 229, 231	sylanbrc 582	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼))
233	48, 52	lspssid 21006	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
234	42, 50, 233	syl2anc 583	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
235	51, 55	lsslinds 21874	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)))
236	235	biimpar 477	. . . . . . . . . 10 ⊢ (((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
237	42, 67, 234, 47, 236	syl31anc 1373	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
238		eqid 2740	. . . . . . . . . . . . 13 ⊢ (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
239	55, 52, 238, 51	lsslsp 21036	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
240	239	eqcomd 2746	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
241	42, 54, 234, 240	syl3anc 1371	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
242	241, 224	eqtr3d 2782	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
243		eqid 2740	. . . . . . . . . 10 ⊢ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
244	145, 243, 238	islbs4 21875	. . . . . . . . 9 ⊢ ((𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ∧ ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))))
245	237, 242, 244	sylanbrc 582	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
246		eqid 2740	. . . . . . . . 9 ⊢ (LBasis‘𝐼) = (LBasis‘𝐼)
247	243, 246	lmimlbs 21879	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ∧ (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
248	232, 245, 247	syl2anc 583	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
249	246	dimval 33613	. . . . . . 7 ⊢ ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
250	31, 248, 249	syl2anc 583	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
251		f1imaeng 9074	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤))
252		hasheni 14397	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
253	251, 252	syl 17	. . . . . . 7 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
254	157, 234, 47, 253	syl3anc 1371	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
255	250, 254	eqtrd 2780	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘(𝑏 ∖ 𝑤)))
256	28, 255	oveq12d 7466	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
257	16, 25, 256	3eqtr4d 2790	. . 3 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
258	4	lbslinds 21876	. . . . . 6 ⊢ (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
259	258, 93	sselid 4006	. . . . 5 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
260	51, 2	lsslinds 21874	. . . . . 6 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉)))
261	260	biimpa 476	. . . . 5 ⊢ (((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
262	98, 101, 109, 259, 261	syl31anc 1373	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
263	23	islinds4 21878	. . . . 5 ⊢ (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
264	263	ad2antrr 725	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
265	262, 264	mpbid 232	. . 3 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)
266	257, 265	r19.29a 3168	. 2 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
267	8, 266	exlimddv 1934	1 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648   class class class wbr 5166  ^◡ccnv 5699  ran crn 5701   ↾ cres 5702   “ cima 5703   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448   ≈ cen 9000   +_𝑒 cxad 13173  ♯chash 14379  Basecbs 17258   ↾_s cress 17287  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772  Grpcgrp 18973  SubGrpcsubg 19160   GrpHom cghm 19252  LSSumclsm 19676  LModclmod 20880  LSubSpclss 20952  LSpanclspn 20992   LMHom clmhm 21041   LMIso clmim 21042  LBasisclbs 21096  LVecclvec 21124  LIndSclinds 21848  dimcldim 33611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-reg 9661  ax-inf2 9710  ax-ac2 10532  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-rpss 7758  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-tpos 8267  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-er 8763  df-map 8886  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-sup 9511  df-oi 9579  df-r1 9833  df-rank 9834  df-dju 9970  df-card 10008  df-acn 10011  df-ac 10185  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-xnn0 12626  df-z 12640  df-dec 12759  df-uz 12904  df-xadd 13176  df-fz 13568  df-fzo 13712  df-seq 14053  df-hash 14380  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ocomp 17332  df-ds 17333  df-hom 17335  df-cco 17336  df-0g 17501  df-gsum 17502  df-prds 17507  df-pws 17509  df-mre 17644  df-mrc 17645  df-mri 17646  df-acs 17647  df-proset 18365  df-drs 18366  df-poset 18383  df-ipo 18598  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-submnd 18819  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-ghm 19253  df-cntz 19357  df-lsm 19678  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-oppr 20360  df-dvdsr 20383  df-unit 20384  df-invr 20414  df-nzr 20539  df-subrg 20597  df-drng 20753  df-lmod 20882  df-lss 20953  df-lsp 20993  df-lmhm 21044  df-lmim 21045  df-lbs 21097  df-lvec 21125  df-sra 21195  df-rgmod 21196  df-dsmm 21775  df-frlm 21790  df-uvc 21826  df-lindf 21849  df-linds 21850  df-dim 33612

This theorem is referenced by:  qusdimsum  33641  lvecendof1f1o  33646