Step | Hyp | Ref
| Expression |
1 | | pwssplit1.b |
. 2
β’ π΅ = (Baseβπ) |
2 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | simp1 1137 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β LMod) |
8 | | simp2 1138 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β π) |
9 | | pwssplit1.y |
. . . 4
β’ π = (π βs π) |
10 | 9 | pwslmod 20581 |
. . 3
β’ ((π β LMod β§ π β π) β π β LMod) |
11 | 7, 8, 10 | syl2anc 585 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β π β LMod) |
12 | | simp3 1139 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β π β π) |
13 | 8, 12 | ssexd 5325 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β π β V) |
14 | | pwssplit1.z |
. . . 4
β’ π = (π βs π) |
15 | 14 | pwslmod 20581 |
. . 3
β’ ((π β LMod β§ π β V) β π β LMod) |
16 | 7, 13, 15 | syl2anc 585 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β π β LMod) |
17 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
18 | 14, 17 | pwssca 17442 |
. . . 4
β’ ((π β LMod β§ π β V) β
(Scalarβπ) =
(Scalarβπ)) |
19 | 7, 13, 18 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
20 | 9, 17 | pwssca 17442 |
. . . 4
β’ ((π β LMod β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
21 | 7, 8, 20 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
22 | 19, 21 | eqtr3d 2775 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
23 | | lmodgrp 20478 |
. . 3
β’ (π β LMod β π β Grp) |
24 | | pwssplit1.c |
. . . 4
β’ πΆ = (Baseβπ) |
25 | | pwssplit1.f |
. . . 4
β’ πΉ = (π₯ β π΅ β¦ (π₯ βΎ π)) |
26 | 9, 14, 1, 24, 25 | pwssplit2 20671 |
. . 3
β’ ((π β Grp β§ π β π β§ π β π) β πΉ β (π GrpHom π)) |
27 | 23, 26 | syl3an1 1164 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β πΉ β (π GrpHom π)) |
28 | | snex 5432 |
. . . . . . . 8
β’ {π} β V |
29 | | xpexg 7737 |
. . . . . . . 8
β’ ((π β π β§ {π} β V) β (π Γ {π}) β V) |
30 | 8, 28, 29 | sylancl 587 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π Γ {π}) β V) |
31 | | vex 3479 |
. . . . . . 7
β’ π β V |
32 | | offres 7970 |
. . . . . . 7
β’ (((π Γ {π}) β V β§ π β V) β (((π Γ {π}) βf (
Β·π βπ)π) βΎ π) = (((π Γ {π}) βΎ π) βf (
Β·π βπ)(π βΎ π))) |
33 | 30, 31, 32 | sylancl 587 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (((π Γ {π}) βf (
Β·π βπ)π) βΎ π) = (((π Γ {π}) βΎ π) βf (
Β·π βπ)(π βΎ π))) |
34 | 33 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (((π Γ {π}) βf (
Β·π βπ)π) βΎ π) = (((π Γ {π}) βΎ π) βf (
Β·π βπ)(π βΎ π))) |
35 | | xpssres 6019 |
. . . . . . . 8
β’ (π β π β ((π Γ {π}) βΎ π) = (π Γ {π})) |
36 | 35 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β ((π Γ {π}) βΎ π) = (π Γ {π})) |
37 | 36 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β ((π Γ {π}) βΎ π) = (π Γ {π})) |
38 | 37 | oveq1d 7424 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (((π Γ {π}) βΎ π) βf (
Β·π βπ)(π βΎ π)) = ((π Γ {π}) βf (
Β·π βπ)(π βΎ π))) |
39 | 34, 38 | eqtrd 2773 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (((π Γ {π}) βf (
Β·π βπ)π) βΎ π) = ((π Γ {π}) βf (
Β·π βπ)(π βΎ π))) |
40 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
41 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
42 | | simpl1 1192 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β π β LMod) |
43 | | simpl2 1193 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β π β π) |
44 | 21 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
45 | 44 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π β (Baseβ(Scalarβπ)) β π β (Baseβ(Scalarβπ)))) |
46 | 45 | biimpar 479 |
. . . . . . 7
β’ (((π β LMod β§ π β π β§ π β π) β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
47 | 46 | adantrr 716 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β π β (Baseβ(Scalarβπ))) |
48 | | simprr 772 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β π β π΅) |
49 | 9, 1, 40, 2, 17, 41, 42, 43, 47, 48 | pwsvscafval 17440 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (π( Β·π
βπ)π) = ((π Γ {π}) βf (
Β·π βπ)π)) |
50 | 49 | reseq1d 5981 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β ((π( Β·π
βπ)π) βΎ π) = (((π Γ {π}) βf (
Β·π βπ)π) βΎ π)) |
51 | 25 | fvtresfn 7001 |
. . . . . 6
β’ (π β π΅ β (πΉβπ) = (π βΎ π)) |
52 | 51 | ad2antll 728 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (πΉβπ) = (π βΎ π)) |
53 | 52 | oveq2d 7425 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β ((π Γ {π}) βf (
Β·π βπ)(πΉβπ)) = ((π Γ {π}) βf (
Β·π βπ)(π βΎ π))) |
54 | 39, 50, 53 | 3eqtr4d 2783 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β ((π( Β·π
βπ)π) βΎ π) = ((π Γ {π}) βf (
Β·π βπ)(πΉβπ))) |
55 | 1, 4, 2, 6 | lmodvscl 20489 |
. . . . . 6
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π β π΅) β (π( Β·π
βπ)π) β π΅) |
56 | 55 | 3expb 1121 |
. . . . 5
β’ ((π β LMod β§ (π β
(Baseβ(Scalarβπ)) β§ π β π΅)) β (π( Β·π
βπ)π) β π΅) |
57 | 11, 56 | sylan 581 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (π( Β·π
βπ)π) β π΅) |
58 | 25 | fvtresfn 7001 |
. . . 4
β’ ((π(
Β·π βπ)π) β π΅ β (πΉβ(π( Β·π
βπ)π)) = ((π( Β·π
βπ)π) βΎ π)) |
59 | 57, 58 | syl 17 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (πΉβ(π( Β·π
βπ)π)) = ((π( Β·π
βπ)π) βΎ π)) |
60 | 13 | adantr 482 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β π β V) |
61 | 9, 14, 1, 24, 25 | pwssplit0 20669 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β πΉ:π΅βΆπΆ) |
62 | 61 | ffvelcdmda 7087 |
. . . . 5
β’ (((π β LMod β§ π β π β§ π β π) β§ π β π΅) β (πΉβπ) β πΆ) |
63 | 62 | adantrl 715 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (πΉβπ) β πΆ) |
64 | 14, 24, 40, 3, 17, 41, 42, 60, 47, 63 | pwsvscafval 17440 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (π( Β·π
βπ)(πΉβπ)) = ((π Γ {π}) βf (
Β·π βπ)(πΉβπ))) |
65 | 54, 59, 64 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π β π β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π΅)) β (πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(πΉβπ))) |
66 | 1, 2, 3, 4, 5, 6, 11, 16, 22, 27, 65 | islmhmd 20650 |
1
β’ ((π β LMod β§ π β π β§ π β π) β πΉ β (π LMHom π)) |