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 ffvelcdmd ⊒ ( ( ( ( ( ( ( ( ( ( ( 𝑉 ∈ 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 β€˜ 𝐼 ) ) )