Theorem dimkerim 33655

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 33648	. . . 4 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4		eqid 2735	. . . . 5 ⊢ (LBasis‘𝐾) = (LBasis‘𝐾)
5	4	lbsex 21185	. . . 4 ⊢ (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
6	3, 5	syl 17	. . 3 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7		n0 4359	. . 3 ⊢ ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
8	6, 7	sylib 218	. 2 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9		simpllr 776	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10		vex 3482	. . . . . . 7 ⊢ 𝑏 ∈ V
11	10	difexi 5336	. . . . . 6 ⊢ (𝑏 ∖ 𝑤) ∈ V
12	11	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ V)
13		disjdif 4478	. . . . . 6 ⊢ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅
14	13	a1i 11	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅)
15		hashunx 14422	. . . . 5 ⊢ ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏 ∖ 𝑤) ∈ V ∧ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
16	9, 12, 14, 15	syl3anc 1370	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
17		simp-4l 783	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LVec)
18		simpr 484	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ 𝑏)
19		undif 4488	. . . . . . 7 ⊢ (𝑤 ⊆ 𝑏 ↔ (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
20	18, 19	sylib 218	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏)
21		simplr 769	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘𝑉))
22	20, 21	eqeltrd 2839	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉))
23		eqid 2735	. . . . . 6 ⊢ (LBasis‘𝑉) = (LBasis‘𝑉)
24	23	dimval 33628	. . . . 5 ⊢ ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
25	17, 22, 24	syl2anc 584	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
26	3	ad3antrrr 730	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐾 ∈ LVec)
27	4	dimval 33628	. . . . . 6 ⊢ ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
28	26, 9, 27	syl2anc 584	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐾) = (♯‘𝑤))
29		dimkerim.i	. . . . . . . . 9 ⊢ 𝐼 = (𝑈 ↾s ran 𝐹)
30	29	imlmhm 33649	. . . . . . . 8 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
31	30	ad3antrrr 730	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐼 ∈ LVec)
32		simp-4r 784	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33		lmhmlmod2 21049	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
34	32, 33	syl 17	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑈 ∈ LMod)
35		lmhmrnlss 21067	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
36	32, 35	syl 17	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37		df-ima 5702	. . . . . . . . . . 11 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
38		imassrn 6091	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹
39	38	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
40	37, 39	eqsstrrid 4045	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹)
41		lveclmod 21123	. . . . . . . . . . . . 13 ⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod)
42	41	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LMod)
43	23	lbslinds 21871	. . . . . . . . . . . . . . 15 ⊢ (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
44	43, 21	sselid 3993	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45		difssd 4147	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ 𝑏)
46		lindsss 21862	. . . . . . . . . . . . . 14 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
47	42, 44, 45, 46	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))
48		eqid 2735	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑉) = (Base‘𝑉)
49	48	linds1 21848	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
50	47, 49	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
51		eqid 2735	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑉) = (LSubSp‘𝑉)
52		eqid 2735	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑉) = (LSpan‘𝑉)
53	48, 51, 52	lspcl 20992	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
54	42, 50, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
55		eqid 2735	. . . . . . . . . . . 12 ⊢ (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
56	51, 55	reslmhm 21069	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
57	32, 54, 56	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈))
58		eqid 2735	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
59	29, 58	reslmhm2b 21071	. . . . . . . . . . 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 1372	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))
62		lmghm 21048	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
63	62	ad4antlr 733	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
64	48, 23	lbsss 21094	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
65	21, 64	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ⊆ (Base‘𝑉))
66	45, 65	sstrd 4006	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉))
67	42, 66, 53	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉))
68	51	lsssubg 20973	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
69	42, 67, 68	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉))
70	55	resghm 19263	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
71	63, 69, 70	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈))
72		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝑈) = (Base‘𝑈)
73	48, 72	lmhmf 21051	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
74	73	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
75	74	ffnd 6738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 Fn (Base‘𝑉))
76	48, 52	lspssv 20999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
77	42, 66, 76	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
78	75, 77	fnssresd 6693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
79		fniniseg 7080	. . . . . . . . . . . . . . . . . . . . . . . 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 580	. . . . . . . . . . . . . . . . . . . . . 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 3996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
86	82	fvresd 6927	. . . . . . . . . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝐹‘𝑥) = 0 )
89		fniniseg 7080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )))
90	89	biimpar 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 }))
91	83, 85, 88, 90	syl12anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (◡𝐹 “ { 0 }))
92	82, 91	elind 4210	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
93		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
94		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘𝐾) = (Base‘𝐾)
95		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (LSpan‘𝐾) = (LSpan‘𝐾)
96	94, 4, 95	lbssp 21096	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
97	93, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
98	41	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
99		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 })
100	99, 1, 51	lmhmkerlss 21068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
101	100	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
102	94, 4	lbsss 21094	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
103	93, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
104		cnvimass 6102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡𝐹 “ { 0 }) ⊆ dom 𝐹
105	104, 73	fssdm 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
106	2, 48	ressbas2 17283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((◡𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
108	107	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) = (Base‘𝐾))
109	103, 108	sseqtrrd 4037	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
110	2, 52, 95, 51	lsslsp 21031	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤))
111	110	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (◡𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
112	98, 101, 109, 111	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
113	97, 112, 108	3eqtr4d 2785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
114	113	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
115	114	ineq2d 4228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })))
116		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘𝑉) = (0g‘𝑉)
117	23, 52, 116	lbsdiflsp0 33654	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
118	117	ad5ant145 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)})
119	115, 118	eqtr3d 2777	. . . . . . . . . . . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ {(0g‘𝑉)})
122	121	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) → 𝑥 ∈ {(0g‘𝑉)}))
123	122	ssrdv 4001	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ⊆ {(0g‘𝑉)})
124	116, 48, 52	0ellsp 33377	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
125	42, 66, 124	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
126		fvexd 6922	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V)
127	125	fvresd 6927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = (𝐹‘(0g‘𝑉)))
128	116, 1	ghmid 19253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
129	62, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 )
130	129	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹‘(0g‘𝑉)) = 0 )
131	127, 130	eqtrd 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 )
132		elsng 4645	. . . . . . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 })
135	78, 125, 134	elpreimad 7079	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
136	135	snssd 4814	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} ⊆ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }))
137	123, 136	eqssd 4013	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘𝑉)})
138		lmodgrp 20882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139		grpmnd 18971	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
140	42, 138, 139	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ Mnd)
141	55, 48, 116	ress0g 18788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 ∈ Mnd ∧ (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
142	140, 125, 77, 141	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
143	142	sneqd 4643	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
144	137, 143	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) = {(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})
145		eqid 2735	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
146		eqid 2735	. . . . . . . . . . . . . . . . 17 ⊢ (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
147	145, 72, 146, 1	kerf1ghm 19278	. . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . 14 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈))
150		eqidd 2736	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
151	55, 48	ressbas2 17283	. . . . . . . . . . . . . . . 16 ⊢ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
152	77, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
153		eqidd 2736	. . . . . . . . . . . . . . 15 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑈) = (Base‘𝑈))
154	150, 152, 153	f1eq123d 6841	. . . . . . . . . . . . . 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 6811	. . . . . . . . . . . . 13 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹)
157	155, 40, 156	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹)
158		f1f1orn 6860	. . . . . . . . . . . 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 784	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = 𝑦)
161	75	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉))
162		simpllr 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤))
163	113	ad8antr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 }))
164	162, 163	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (◡𝐹 “ { 0 }))
165		fniniseg 7080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (◡𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹‘𝑢) = 0 )))
166	165	simplbda 499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑢) = 0 )
167	161, 164, 166	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑢) = 0 )
168	167	oveq1d 7446	. . . . . . . . . . . . . . . . . . 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 6911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝑉)𝑣)))
171	63	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
172	48, 52	lspss 21000	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
173	42, 65, 18, 172	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
174	48, 23, 52	lbssp 21096	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
175	21, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176	173, 175	sseqtrd 4036	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
177	176	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
178	177	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
179	178, 162	sseldd 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉))
180	77	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
181	180	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
182		simplr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
183	181, 182	sseldd 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184		eqid 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑉) = (+g‘𝑉)
185		eqid 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (+g‘𝑈) = (+g‘𝑈)
186	48, 184, 185	ghmlin 19252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
187	171, 179, 183, 186	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)))
188	170, 187	eqtr2d 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑥))
189		lmhmlvec2 33647	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190	189	lvecgrpd 21125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
191	190	ad9antr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑈 ∈ Grp)
192	74	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
193	192, 183	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (Base‘𝑈))
194	72, 185, 1, 191, 193	grplidd 19000	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ( 0 (+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑣))
195	168, 188, 194	3eqtr3d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘𝑣))
196	160, 195	eqtr3d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 = (𝐹‘𝑣))
197	161, 183, 182	fnfvimad 7254	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
198	196, 197	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
199		simp-7l 789	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑉 ∈ LVec)
200		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
201	109	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (◡𝐹 “ { 0 }))
202	105	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡𝐹 “ { 0 }) ⊆ (Base‘𝑉))
203	201, 202	sstrd 4006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (Base‘𝑉))
204		eqid 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (LSSum‘𝑉) = (LSSum‘𝑉)
205	48, 52, 204	lsmsp2 21104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
206	42, 203, 66, 205	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))))
207	20	fveq2d 6911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘𝑏))
208	206, 207, 175	3eqtrrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
209	208	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
210	200, 209	eleqtrd 2841	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
211	48, 184, 204	lsmelvalx 19673	. . . . . . . . . . . . . . . . . 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 1372	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))
214	198, 213	r19.29vva 3214	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
215		fvelrnb 6969	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦))
216	215	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
217	75, 216	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)
218	214, 217	r19.29a 3160	. . . . . . . . . . . . . 14 ⊢ ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
219	39, 218	eqelssd 4017	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
220	37, 219	eqtr3id 2789	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹)
221	220	f1oeq3d 6846	. . . . . . . . . . 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 584	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉))
224	223, 151	syl 17	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
225		frn 6744	. . . . . . . . . . . 12 ⊢ (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
226	29, 72	ressbas2 17283	. . . . . . . . . . . 12 ⊢ (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
227	32, 73, 225, 226	4syl 19	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 = (Base‘𝐼))
228	150, 224, 227	f1oeq123d 6843	. . . . . . . . . 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 2735	. . . . . . . . . 10 ⊢ (Base‘𝐼) = (Base‘𝐼)
231	145, 230	islmim 21079	. . . . . . . . 9 ⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼)))
232	61, 229, 231	sylanbrc 583	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼))
233	48, 52	lspssid 21001	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
234	42, 50, 233	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
235	51, 55	lsslinds 21869	. . . . . . . . . . 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 1372	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
238		eqid 2735	. . . . . . . . . . . . 13 ⊢ (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
239	55, 52, 238, 51	lsslsp 21031	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))
240	239	eqcomd 2741	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
241	42, 54, 234, 240	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)))
242	241, 224	eqtr3d 2777	. . . . . . . . 9 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
243		eqid 2735	. . . . . . . . . 10 ⊢ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))
244	145, 243, 238	islbs4 21870	. . . . . . . . 9 ⊢ ((𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ∧ ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))))
245	237, 242, 244	sylanbrc 583	. . . . . . . 8 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))
246		eqid 2735	. . . . . . . . 9 ⊢ (LBasis‘𝐼) = (LBasis‘𝐼)
247	243, 246	lmimlbs 21874	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ∧ (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
248	232, 245, 247	syl2anc 584	. . . . . . 7 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼))
249	246	dimval 33628	. . . . . . 7 ⊢ ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
250	31, 248, 249	syl2anc 584	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))))
251		f1imaeng 9053	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤))
252		hasheni 14384	. . . . . . . 8 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
253	251, 252	syl 17	. . . . . . 7 ⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
254	157, 234, 47, 253	syl3anc 1370	. . . . . 6 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤)))
255	250, 254	eqtrd 2775	. . . . 5 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘(𝑏 ∖ 𝑤)))
256	28, 255	oveq12d 7449	. . . 4 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤))))
257	16, 25, 256	3eqtr4d 2785	. . 3 ⊢ (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
258	4	lbslinds 21871	. . . . . 6 ⊢ (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
259	258, 93	sselid 3993	. . . . 5 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
260	51, 2	lsslinds 21869	. . . . . 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 1372	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
263	23	islinds4 21873	. . . . 5 ⊢ (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
264	263	ad2antrr 726	. . . 4 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏))
265	262, 264	mpbid 232	. . 3 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)
266	257, 265	r19.29a 3160	. 2 ⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
267	8, 266	exlimddv 1933	1 ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1537  ∃wex 1776   ∈ wcel 2106   ≠ wne 2938  ∃wrex 3068  Vcvv 3478   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  {csn 4631   class class class wbr 5148  ^◡ccnv 5688  ran crn 5690   ↾ cres 5691   “ cima 5692   Fn wfn 6558  ⟶wf 6559  –1-1→wf1 6560  –1-1-onto→wf1o 6562  ‘cfv 6563  (class class class)co 7431   ≈ cen 8981   +_𝑒 cxad 13150  ♯chash 14366  Basecbs 17245   ↾_s cress 17274  +_gcplusg 17298  0_gc0g 17486  Mndcmnd 18760  Grpcgrp 18964  SubGrpcsubg 19151   GrpHom cghm 19243  LSSumclsm 19667  LModclmod 20875  LSubSpclss 20947  LSpanclspn 20987   LMHom clmhm 21036   LMIso clmim 21037  LBasisclbs 21091  LVecclvec 21119  LIndSclinds 21843  dimcldim 33626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-reg 9630  ax-inf2 9679  ax-ac2 10501  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-rpss 7742  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-er 8744  df-map 8867  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-sup 9480  df-oi 9548  df-r1 9802  df-rank 9803  df-dju 9939  df-card 9977  df-acn 9980  df-ac 10154  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-xnn0 12598  df-z 12612  df-dec 12732  df-uz 12877  df-xadd 13153  df-fz 13545  df-fzo 13692  df-seq 14040  df-hash 14367  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ocomp 17319  df-ds 17320  df-hom 17322  df-cco 17323  df-0g 17488  df-gsum 17489  df-prds 17494  df-pws 17496  df-mre 17631  df-mrc 17632  df-mri 17633  df-acs 17634  df-proset 18352  df-drs 18353  df-poset 18371  df-ipo 18586  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-mhm 18809  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-subg 19154  df-ghm 19244  df-cntz 19348  df-lsm 19669  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-ring 20253  df-oppr 20351  df-dvdsr 20374  df-unit 20375  df-invr 20405  df-nzr 20530  df-subrg 20587  df-drng 20748  df-lmod 20877  df-lss 20948  df-lsp 20988  df-lmhm 21039  df-lmim 21040  df-lbs 21092  df-lvec 21120  df-sra 21190  df-rgmod 21191  df-dsmm 21770  df-frlm 21785  df-uvc 21821  df-lindf 21844  df-linds 21845  df-dim 33627

This theorem is referenced by:  qusdimsum  33656  lvecendof1f1o  33661