Step |
Hyp |
Ref |
Expression |
1 |
|
quslmod.n |
โข ๐ = ( ๐ /s ( ๐ ~QG ๐บ ) ) |
2 |
|
quslmod.v |
โข ๐ = ( Base โ ๐ ) |
3 |
|
quslmod.1 |
โข ( ๐ โ ๐ โ LMod ) |
4 |
|
quslmod.2 |
โข ( ๐ โ ๐บ โ ( LSubSp โ ๐ ) ) |
5 |
|
quslmhm.f |
โข ๐น = ( ๐ฅ โ ๐ โฆ [ ๐ฅ ] ( ๐ ~QG ๐บ ) ) |
6 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
7 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
8 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
9 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
10 |
|
eqid |
โข ( Base โ ( Scalar โ ๐ ) ) = ( Base โ ( Scalar โ ๐ ) ) |
11 |
1 2 3 4
|
quslmod |
โข ( ๐ โ ๐ โ LMod ) |
12 |
1
|
a1i |
โข ( ๐ โ ๐ = ( ๐ /s ( ๐ ~QG ๐บ ) ) ) |
13 |
2
|
a1i |
โข ( ๐ โ ๐ = ( Base โ ๐ ) ) |
14 |
|
ovexd |
โข ( ๐ โ ( ๐ ~QG ๐บ ) โ V ) |
15 |
12 13 14 3 8
|
quss |
โข ( ๐ โ ( Scalar โ ๐ ) = ( Scalar โ ๐ ) ) |
16 |
15
|
eqcomd |
โข ( ๐ โ ( Scalar โ ๐ ) = ( Scalar โ ๐ ) ) |
17 |
|
eqid |
โข ( LSubSp โ ๐ ) = ( LSubSp โ ๐ ) |
18 |
17
|
lsssubg |
โข ( ( ๐ โ LMod โง ๐บ โ ( LSubSp โ ๐ ) ) โ ๐บ โ ( SubGrp โ ๐ ) ) |
19 |
3 4 18
|
syl2anc |
โข ( ๐ โ ๐บ โ ( SubGrp โ ๐ ) ) |
20 |
|
lmodabl |
โข ( ๐ โ LMod โ ๐ โ Abel ) |
21 |
|
ablnsg |
โข ( ๐ โ Abel โ ( NrmSGrp โ ๐ ) = ( SubGrp โ ๐ ) ) |
22 |
3 20 21
|
3syl |
โข ( ๐ โ ( NrmSGrp โ ๐ ) = ( SubGrp โ ๐ ) ) |
23 |
19 22
|
eleqtrrd |
โข ( ๐ โ ๐บ โ ( NrmSGrp โ ๐ ) ) |
24 |
2 1 5
|
qusghm |
โข ( ๐บ โ ( NrmSGrp โ ๐ ) โ ๐น โ ( ๐ GrpHom ๐ ) ) |
25 |
23 24
|
syl |
โข ( ๐ โ ๐น โ ( ๐ GrpHom ๐ ) ) |
26 |
12 13 5 14 3
|
qusval |
โข ( ๐ โ ๐ = ( ๐น โs ๐ ) ) |
27 |
12 13 5 14 3
|
quslem |
โข ( ๐ โ ๐น : ๐ โontoโ ( ๐ / ( ๐ ~QG ๐บ ) ) ) |
28 |
|
eqid |
โข ( ๐ ~QG ๐บ ) = ( ๐ ~QG ๐บ ) |
29 |
3
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ๐ โ LMod ) |
30 |
4
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ๐บ โ ( LSubSp โ ๐ ) ) |
31 |
|
simpr1 |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ๐ โ ( Base โ ( Scalar โ ๐ ) ) ) |
32 |
|
simpr2 |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ๐ข โ ๐ ) |
33 |
|
simpr3 |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ๐ฃ โ ๐ ) |
34 |
2 28 10 6 29 30 31 1 7 5 32 33
|
qusvscpbl |
โข ( ( ๐ โง ( ๐ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ข โ ๐ โง ๐ฃ โ ๐ ) ) โ ( ( ๐น โ ๐ข ) = ( ๐น โ ๐ฃ ) โ ( ๐น โ ( ๐ ( ยท๐ โ ๐ ) ๐ข ) ) = ( ๐น โ ( ๐ ( ยท๐ โ ๐ ) ๐ฃ ) ) ) ) |
35 |
26 13 27 3 8 10 6 7 34
|
imasvscaval |
โข ( ( ๐ โง ๐ฆ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ง โ ๐ ) โ ( ๐ฆ ( ยท๐ โ ๐ ) ( ๐น โ ๐ง ) ) = ( ๐น โ ( ๐ฆ ( ยท๐ โ ๐ ) ๐ง ) ) ) |
36 |
35
|
3expb |
โข ( ( ๐ โง ( ๐ฆ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ง โ ๐ ) ) โ ( ๐ฆ ( ยท๐ โ ๐ ) ( ๐น โ ๐ง ) ) = ( ๐น โ ( ๐ฆ ( ยท๐ โ ๐ ) ๐ง ) ) ) |
37 |
36
|
eqcomd |
โข ( ( ๐ โง ( ๐ฆ โ ( Base โ ( Scalar โ ๐ ) ) โง ๐ง โ ๐ ) ) โ ( ๐น โ ( ๐ฆ ( ยท๐ โ ๐ ) ๐ง ) ) = ( ๐ฆ ( ยท๐ โ ๐ ) ( ๐น โ ๐ง ) ) ) |
38 |
2 6 7 8 9 10 3 11 16 25 37
|
islmhmd |
โข ( ๐ โ ๐น โ ( ๐ LMHom ๐ ) ) |