Metamath Proof Explorer

Theorem dimkerim

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

Ref Expression
Hypotheses dimkerim.0 ⊢ 0 = ( 0g ‘ 𝑈 )
dimkerim.k ⊢ 𝐾 = ( 𝑉 ↾s ( ◡ 𝐹 “ { 0 } ) )
dimkerim.i ⊢ 𝐼 = ( 𝑈 ↾s ran 𝐹 )
Assertion dimkerim ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ( dim ‘ 𝑉 ) = ( ( dim ‘ 𝐾 ) +𝑒 ( dim ‘ 𝐼 ) ) )

Proof

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