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 fnssres ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑉 ) ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ⊆ ( Base ‘ 𝑉 ) ) → ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) Fn ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
79 75 77 78 syl2anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) Fn ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
80 fniniseg ⊢ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) Fn ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ↔ ( 𝑥 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ‘ 𝑥 ) = 0 ) ) )
81 80 biimpa ⊢ ( ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) Fn ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ‘ 𝑥 ) = 0 ) )
82 79 81 sylan ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ‘ 𝑥 ) = 0 ) )
83 82 simpld ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → 𝑥 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
84 75 adantr ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → 𝐹 Fn ( Base ‘ 𝑉 ) )
85 77 adantr ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ⊆ ( Base ‘ 𝑉 ) )
86 85 83 sseldd ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑉 ) )
87 83 fvresd ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
88 82 simprd ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ‘ 𝑥 ) = 0 )
89 87 88 eqtr3d ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
90 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝑉 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
91 90 biimpar ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
92 84 86 89 91 syl12anc ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
93 83 92 elind ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑥 ∈ ( ◡ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ { 0 } ) ) → 𝑥 ∈ ( ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∩ ( ◡ 𝐹 “ { 0 } ) ) )
94 simpr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑤 ∈ ( LBasis ‘ 𝐾 ) )
95 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
96 eqid ⊢ ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐾 )
97 95 5 96 lbssp ⊢ ( 𝑤 ∈ ( LBasis ‘ 𝐾 ) → ( ( LSpan ‘ 𝐾 ) ‘ 𝑤 ) = ( Base ‘ 𝐾 ) )
98 94 97 syl ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( ( LSpan ‘ 𝐾 ) ‘ 𝑤 ) = ( Base ‘ 𝐾 ) )
99 41 ad2antrr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑉 ∈ LMod )
100 eqid ⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } )
101 100 1 51 lmhmkerlss ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) )
102 101 ad2antlr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) )
103 95 5 lbsss ⊢ ( 𝑤 ∈ ( LBasis ‘ 𝐾 ) → 𝑤 ⊆ ( Base ‘ 𝐾 ) )
104 94 103 syl ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑤 ⊆ ( Base ‘ 𝐾 ) )
105 cnvimass ⊢ ( ◡ 𝐹 “ { 0 } ) ⊆ dom 𝐹
106 105 73 fssdm ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ( ◡ 𝐹 “ { 0 } ) ⊆ ( Base ‘ 𝑉 ) )
107 2 48 ressbas2 ⊢ ( ( ◡ 𝐹 “ { 0 } ) ⊆ ( Base ‘ 𝑉 ) → ( ◡ 𝐹 “ { 0 } ) = ( Base ‘ 𝐾 ) )
108 106 107 syl ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ( ◡ 𝐹 “ { 0 } ) = ( Base ‘ 𝐾 ) )
109 108 ad2antlr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( ◡ 𝐹 “ { 0 } ) = ( Base ‘ 𝐾 ) )
110 104 109 sseqtrrd ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ { 0 } ) )
111 2 52 96 51 lsslsp ⊢ ( ( 𝑉 ∈ LMod ∧ ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) ∧ 𝑤 ⊆ ( ◡ 𝐹 “ { 0 } ) ) → ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) = ( ( LSpan ‘ 𝐾 ) ‘ 𝑤 ) )
112 99 102 110 111 syl3anc ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) = ( ( LSpan ‘ 𝐾 ) ‘ 𝑤 ) )
113 98 112 109 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 93 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 79 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 lveclmod ⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
191 lmodgrp ⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Grp )
192 189 190 191 3syl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝑈 ∈ Grp )
193 192 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → 𝑈 ∈ Grp )
194 74 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑈 ) )
195 194 183 ffvelrnd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ( Base ‘ 𝑈 ) )
196 72 185 1 grplid ⊢ ( ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( Base ‘ 𝑈 ) ) → ( 0 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 ‘ 𝑣 ) )
197 193 195 196 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → ( 0 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 ‘ 𝑣 ) )
198 168 188 197 3eqtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
199 160 198 eqtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → 𝑦 = ( 𝐹 ‘ 𝑣 ) )
200 161 183 182 fnfvimad ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 “ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
201 199 200 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ∧ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ) ∧ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) → 𝑦 ∈ ( 𝐹 “ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
202 simp-7l ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑉 ∈ LVec )
203 simplr ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ ( Base ‘ 𝑉 ) )
204 110 ad2antrr ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → 𝑤 ⊆ ( ◡ 𝐹 “ { 0 } ) )
205 106 ad4antlr ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ◡ 𝐹 “ { 0 } ) ⊆ ( Base ‘ 𝑉 ) )
206 204 205 sstrd ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → 𝑤 ⊆ ( Base ‘ 𝑉 ) )
207 eqid ⊢ ( LSSum ‘ 𝑉 ) = ( LSSum ‘ 𝑉 )
208 48 52 207 lsmsp2 ⊢ ( ( 𝑉 ∈ LMod ∧ 𝑤 ⊆ ( Base ‘ 𝑉 ) ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( Base ‘ 𝑉 ) ) → ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) = ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑤 ∪ ( 𝑏 ∖ 𝑤 ) ) ) )
209 42 206 66 208 syl3anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) = ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑤 ∪ ( 𝑏 ∖ 𝑤 ) ) ) )
210 21 fveq2d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑤 ∪ ( 𝑏 ∖ 𝑤 ) ) ) = ( ( LSpan ‘ 𝑉 ) ‘ 𝑏 ) )
211 209 210 175 3eqtrrd ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( Base ‘ 𝑉 ) = ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
212 211 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( Base ‘ 𝑉 ) = ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
213 203 212 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
214 48 184 207 lsmelvalx ⊢ ( ( 𝑉 ∈ LVec ∧ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ⊆ ( Base ‘ 𝑉 ) ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ⊆ ( Base ‘ 𝑉 ) ) → ( 𝑥 ∈ ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ↔ ∃ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ∃ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) ) )
215 214 biimpa ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ⊆ ( Base ‘ 𝑉 ) ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ⊆ ( Base ‘ 𝑉 ) ) ∧ 𝑥 ∈ ( ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ( LSSum ‘ 𝑉 ) ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) → ∃ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ∃ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) )
216 202 177 180 213 215 syl31anc ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ∃ 𝑢 ∈ ( ( LSpan ‘ 𝑉 ) ‘ 𝑤 ) ∃ 𝑣 ∈ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) 𝑥 = ( 𝑢 ( +g ‘ 𝑉 ) 𝑣 ) )
217 201 216 r19.29vva ⊢ ( ( ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ ( 𝐹 “ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
218 fvelrnb ⊢ ( 𝐹 Fn ( Base ‘ 𝑉 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑉 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
219 218 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑉 ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑥 ∈ ( Base ‘ 𝑉 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 )
220 75 219 sylan ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑥 ∈ ( Base ‘ 𝑉 ) ( 𝐹 ‘ 𝑥 ) = 𝑦 )
221 217 220 r19.29a ⊢ ( ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ( 𝐹 “ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
222 39 221 eqelssd ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝐹 “ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) = ran 𝐹 )
223 37 222 eqtr3id ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ran ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) = ran 𝐹 )
224 223 f1oeq3d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1-onto→ ran ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ↔ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1-onto→ ran 𝐹 ) )
225 159 224 mpbid ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1-onto→ ran 𝐹 )
226 42 50 76 syl2anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ⊆ ( Base ‘ 𝑉 ) )
227 226 151 syl ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) = ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) )
228 frn ⊢ ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑈 ) → ran 𝐹 ⊆ ( Base ‘ 𝑈 ) )
229 3 72 ressbas2 ⊢ ( ran 𝐹 ⊆ ( Base ‘ 𝑈 ) → ran 𝐹 = ( Base ‘ 𝐼 ) )
230 73 228 229 3syl ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ran 𝐹 = ( Base ‘ 𝐼 ) )
231 32 230 syl ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ran 𝐹 = ( Base ‘ 𝐼 ) )
232 150 227 231 f1oeq123d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1-onto→ ran 𝐹 ↔ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) –1-1-onto→ ( Base ‘ 𝐼 ) ) )
233 225 232 mpbid ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) –1-1-onto→ ( Base ‘ 𝐼 ) )
234 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
235 145 234 islmim ⊢ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∈ ( ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) LMIso 𝐼 ) ↔ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∈ ( ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) LMHom 𝐼 ) ∧ ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) –1-1-onto→ ( Base ‘ 𝐼 ) ) )
236 61 233 235 sylanbrc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∈ ( ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) LMIso 𝐼 ) )
237 48 52 lspssid ⊢ ( ( 𝑉 ∈ LMod ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( Base ‘ 𝑉 ) ) → ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
238 42 50 237 syl2anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
239 51 55 lsslinds ⊢ ( ( 𝑉 ∈ LMod ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LSubSp ‘ 𝑉 ) ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) → ( ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ↔ ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ 𝑉 ) ) )
240 239 biimpar ⊢ ( ( ( 𝑉 ∈ LMod ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LSubSp ‘ 𝑉 ) ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∧ ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ 𝑉 ) ) → ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) )
241 42 67 238 47 240 syl31anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) )
242 eqid ⊢ ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) = ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
243 55 52 242 51 lsslsp ⊢ ( ( 𝑉 ∈ LMod ∧ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LSubSp ‘ 𝑉 ) ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) = ( ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
244 42 54 238 243 syl3anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) = ( ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ‘ ( 𝑏 ∖ 𝑤 ) ) )
245 244 227 eqtr3d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ‘ ( 𝑏 ∖ 𝑤 ) ) = ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) )
246 eqid ⊢ ( LBasis ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) = ( LBasis ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
247 145 246 242 islbs4 ⊢ ( ( 𝑏 ∖ 𝑤 ) ∈ ( LBasis ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ↔ ( ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ∧ ( ( LSpan ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ‘ ( 𝑏 ∖ 𝑤 ) ) = ( Base ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ) )
248 241 245 247 sylanbrc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( 𝑏 ∖ 𝑤 ) ∈ ( LBasis ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) )
249 eqid ⊢ ( LBasis ‘ 𝐼 ) = ( LBasis ‘ 𝐼 )
250 246 249 lmimlbs ⊢ ( ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ∈ ( ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) LMIso 𝐼 ) ∧ ( 𝑏 ∖ 𝑤 ) ∈ ( LBasis ‘ ( 𝑉 ↾s ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) ) ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LBasis ‘ 𝐼 ) )
251 236 248 250 syl2anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LBasis ‘ 𝐼 ) )
252 249 dimval ⊢ ( ( 𝐼 ∈ LVec ∧ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ∈ ( LBasis ‘ 𝐼 ) ) → ( dim ‘ 𝐼 ) = ( ♯ ‘ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ) )
253 31 251 252 syl2anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( dim ‘ 𝐼 ) = ( ♯ ‘ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ) )
254 f1imaeng ⊢ ( ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1→ ran 𝐹 ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ 𝑉 ) ) → ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ≈ ( 𝑏 ∖ 𝑤 ) )
255 hasheni ⊢ ( ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ≈ ( 𝑏 ∖ 𝑤 ) → ( ♯ ‘ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ) = ( ♯ ‘ ( 𝑏 ∖ 𝑤 ) ) )
256 254 255 syl ⊢ ( ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) : ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) –1-1→ ran 𝐹 ∧ ( 𝑏 ∖ 𝑤 ) ⊆ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ∧ ( 𝑏 ∖ 𝑤 ) ∈ ( LIndS ‘ 𝑉 ) ) → ( ♯ ‘ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ) = ( ♯ ‘ ( 𝑏 ∖ 𝑤 ) ) )
257 157 238 47 256 syl3anc ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ♯ ‘ ( ( 𝐹 ↾ ( ( LSpan ‘ 𝑉 ) ‘ ( 𝑏 ∖ 𝑤 ) ) ) “ ( 𝑏 ∖ 𝑤 ) ) ) = ( ♯ ‘ ( 𝑏 ∖ 𝑤 ) ) )
258 253 257 eqtrd ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( dim ‘ 𝐼 ) = ( ♯ ‘ ( 𝑏 ∖ 𝑤 ) ) )
259 29 258 oveq12d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( ( dim ‘ 𝐾 ) +𝑒 ( dim ‘ 𝐼 ) ) = ( ( ♯ ‘ 𝑤 ) +𝑒 ( ♯ ‘ ( 𝑏 ∖ 𝑤 ) ) ) )
260 17 26 259 3eqtr4d ⊢ ( ( ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑤 ⊆ 𝑏 ) → ( dim ‘ 𝑉 ) = ( ( dim ‘ 𝐾 ) +𝑒 ( dim ‘ 𝐼 ) ) )
261 5 lbslinds ⊢ ( LBasis ‘ 𝐾 ) ⊆ ( LIndS ‘ 𝐾 )
262 261 94 sselid ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑤 ∈ ( LIndS ‘ 𝐾 ) )
263 51 2 lsslinds ⊢ ( ( 𝑉 ∈ LMod ∧ ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) ∧ 𝑤 ⊆ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝑤 ∈ ( LIndS ‘ 𝐾 ) ↔ 𝑤 ∈ ( LIndS ‘ 𝑉 ) ) )
264 263 biimpa ⊢ ( ( ( 𝑉 ∈ LMod ∧ ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) ∧ 𝑤 ⊆ ( ◡ 𝐹 “ { 0 } ) ) ∧ 𝑤 ∈ ( LIndS ‘ 𝐾 ) ) → 𝑤 ∈ ( LIndS ‘ 𝑉 ) )
265 99 102 110 262 264 syl31anc ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → 𝑤 ∈ ( LIndS ‘ 𝑉 ) )
266 24 islinds4 ⊢ ( 𝑉 ∈ LVec → ( 𝑤 ∈ ( LIndS ‘ 𝑉 ) ↔ ∃ 𝑏 ∈ ( LBasis ‘ 𝑉 ) 𝑤 ⊆ 𝑏 ) )
267 266 ad2antrr ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( 𝑤 ∈ ( LIndS ‘ 𝑉 ) ↔ ∃ 𝑏 ∈ ( LBasis ‘ 𝑉 ) 𝑤 ⊆ 𝑏 ) )
268 265 267 mpbid ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ∃ 𝑏 ∈ ( LBasis ‘ 𝑉 ) 𝑤 ⊆ 𝑏 )
269 260 268 r19.29a ⊢ ( ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝐾 ) ) → ( dim ‘ 𝑉 ) = ( ( dim ‘ 𝐾 ) +𝑒 ( dim ‘ 𝐼 ) ) )
270 9 269 exlimddv ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ( dim ‘ 𝑉 ) = ( ( dim ‘ 𝐾 ) +𝑒 ( dim ‘ 𝐼 ) ) )