Step |
Hyp |
Ref |
Expression |
1 |
|
frlmup4.r |
โข ๐
= ( Scalar โ ๐ ) |
2 |
|
frlmup4.f |
โข ๐น = ( ๐
freeLMod ๐ผ ) |
3 |
|
frlmup4.u |
โข ๐ = ( ๐
unitVec ๐ผ ) |
4 |
|
frlmup4.c |
โข ๐ถ = ( Base โ ๐ ) |
5 |
|
eqid |
โข ( Base โ ๐น ) = ( Base โ ๐น ) |
6 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
7 |
|
eqid |
โข ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) = ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) |
8 |
|
simp1 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ โ LMod ) |
9 |
|
simp2 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ผ โ ๐ ) |
10 |
1
|
a1i |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐
= ( Scalar โ ๐ ) ) |
11 |
|
simp3 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ด : ๐ผ โถ ๐ถ ) |
12 |
2 5 4 6 7 8 9 10 11
|
frlmup1 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐น LMHom ๐ ) ) |
13 |
|
ovex |
โข ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) โ V |
14 |
13 7
|
fnmpti |
โข ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) Fn ( Base โ ๐น ) |
15 |
1
|
lmodring |
โข ( ๐ โ LMod โ ๐
โ Ring ) |
16 |
15
|
3ad2ant1 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐
โ Ring ) |
17 |
3 2 5
|
uvcff |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ๐ : ๐ผ โถ ( Base โ ๐น ) ) |
18 |
16 9 17
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ : ๐ผ โถ ( Base โ ๐น ) ) |
19 |
18
|
ffnd |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ Fn ๐ผ ) |
20 |
18
|
frnd |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ran ๐ โ ( Base โ ๐น ) ) |
21 |
|
fnco |
โข ( ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) Fn ( Base โ ๐น ) โง ๐ Fn ๐ผ โง ran ๐ โ ( Base โ ๐น ) ) โ ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) Fn ๐ผ ) |
22 |
14 19 20 21
|
mp3an2i |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) Fn ๐ผ ) |
23 |
|
ffn |
โข ( ๐ด : ๐ผ โถ ๐ถ โ ๐ด Fn ๐ผ ) |
24 |
23
|
3ad2ant3 |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ๐ด Fn ๐ผ ) |
25 |
18
|
adantr |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ : ๐ผ โถ ( Base โ ๐น ) ) |
26 |
25
|
ffnd |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ Fn ๐ผ ) |
27 |
|
simpr |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ฆ โ ๐ผ ) |
28 |
|
fvco2 |
โข ( ( ๐ Fn ๐ผ โง ๐ฆ โ ๐ผ ) โ ( ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) โ ๐ฆ ) = ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐ โ ๐ฆ ) ) ) |
29 |
26 27 28
|
syl2anc |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ( ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) โ ๐ฆ ) = ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐ โ ๐ฆ ) ) ) |
30 |
|
simpl1 |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ โ LMod ) |
31 |
|
simpl2 |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ผ โ ๐ ) |
32 |
1
|
a1i |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐
= ( Scalar โ ๐ ) ) |
33 |
|
simpl3 |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ๐ด : ๐ผ โถ ๐ถ ) |
34 |
2 5 4 6 7 30 31 32 33 27 3
|
frlmup2 |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐ โ ๐ฆ ) ) = ( ๐ด โ ๐ฆ ) ) |
35 |
29 34
|
eqtrd |
โข ( ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โง ๐ฆ โ ๐ผ ) โ ( ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) โ ๐ฆ ) = ( ๐ด โ ๐ฆ ) ) |
36 |
22 24 35
|
eqfnfvd |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) = ๐ด ) |
37 |
|
coeq1 |
โข ( ๐ = ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐ โ ๐ ) = ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) ) |
38 |
37
|
eqeq1d |
โข ( ๐ = ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ( ๐ โ ๐ ) = ๐ด โ ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) = ๐ด ) ) |
39 |
38
|
rspcev |
โข ( ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ( ๐น LMHom ๐ ) โง ( ( ๐ฅ โ ( Base โ ๐น ) โฆ ( ๐ ฮฃg ( ๐ฅ โf ( ยท๐ โ ๐ ) ๐ด ) ) ) โ ๐ ) = ๐ด ) โ โ ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) |
40 |
12 36 39
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ โ ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) |
41 |
18
|
ffund |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ Fun ๐ ) |
42 |
|
funcoeqres |
โข ( ( Fun ๐ โง ( ๐ โ ๐ ) = ๐ด ) โ ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) |
43 |
42
|
ex |
โข ( Fun ๐ โ ( ( ๐ โ ๐ ) = ๐ด โ ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) ) |
44 |
43
|
ralrimivw |
โข ( Fun ๐ โ โ ๐ โ ( ๐น LMHom ๐ ) ( ( ๐ โ ๐ ) = ๐ด โ ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) ) |
45 |
41 44
|
syl |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ โ ๐ โ ( ๐น LMHom ๐ ) ( ( ๐ โ ๐ ) = ๐ด โ ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) ) |
46 |
|
eqid |
โข ( LBasis โ ๐น ) = ( LBasis โ ๐น ) |
47 |
2 3 46
|
frlmlbs |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ran ๐ โ ( LBasis โ ๐น ) ) |
48 |
16 9 47
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ran ๐ โ ( LBasis โ ๐น ) ) |
49 |
|
eqid |
โข ( LSpan โ ๐น ) = ( LSpan โ ๐น ) |
50 |
5 46 49
|
lbssp |
โข ( ran ๐ โ ( LBasis โ ๐น ) โ ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) ) |
51 |
48 50
|
syl |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) ) |
52 |
5 49
|
lspextmo |
โข ( ( ran ๐ โ ( Base โ ๐น ) โง ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) ) โ โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) |
53 |
20 51 52
|
syl2anc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) |
54 |
|
rmoim |
โข ( โ ๐ โ ( ๐น LMHom ๐ ) ( ( ๐ โ ๐ ) = ๐ด โ ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) ) โ ( โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โพ ran ๐ ) = ( ๐ด โ โก ๐ ) โ โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) ) |
55 |
45 53 54
|
sylc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) |
56 |
|
reu5 |
โข ( โ! ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด โ ( โ ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด โง โ* ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) ) |
57 |
40 55 56
|
sylanbrc |
โข ( ( ๐ โ LMod โง ๐ผ โ ๐ โง ๐ด : ๐ผ โถ ๐ถ ) โ โ! ๐ โ ( ๐น LMHom ๐ ) ( ๐ โ ๐ ) = ๐ด ) |