Step | Hyp | Ref
| Expression |
1 | | simpl2 1192 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β π β LMod) |
2 | | lincresunit.e |
. . . . . . . . . 10
β’ πΈ = (Baseβπ
) |
3 | | lincresunit.r |
. . . . . . . . . . 11
β’ π
= (Scalarβπ) |
4 | 3 | fveq2i 6845 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
5 | 2, 4 | eqtri 2764 |
. . . . . . . . 9
β’ πΈ =
(Baseβ(Scalarβπ)) |
6 | 5 | oveq1i 7367 |
. . . . . . . 8
β’ (πΈ βm π) =
((Baseβ(Scalarβπ)) βm π) |
7 | 6 | eleq2i 2829 |
. . . . . . 7
β’ (πΉ β (πΈ βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
8 | 7 | biimpi 215 |
. . . . . 6
β’ (πΉ β (πΈ βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
9 | 8 | 3ad2ant1 1133 |
. . . . 5
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 ) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
10 | 9 | adantl 482 |
. . . 4
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΉ β
((Baseβ(Scalarβπ)) βm π)) |
11 | | difssd 4092 |
. . . 4
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π β {π}) β π) |
12 | | elmapssres 8805 |
. . . 4
β’ ((πΉ β
((Baseβ(Scalarβπ)) βm π) β§ (π β {π}) β π) β (πΉ βΎ (π β {π})) β ((Baseβ(Scalarβπ)) βm (π β {π}))) |
13 | 10, 11, 12 | syl2anc 584 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (πΉ βΎ (π β {π})) β ((Baseβ(Scalarβπ)) βm (π β {π}))) |
14 | | elpwi 4567 |
. . . . . . . 8
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
15 | 14 | ssdifssd 4102 |
. . . . . . 7
β’ (π β π«
(Baseβπ) β
(π β {π}) β (Baseβπ)) |
16 | | difexg 5284 |
. . . . . . . 8
β’ (π β π«
(Baseβπ) β
(π β {π}) β V) |
17 | | elpwg 4563 |
. . . . . . . 8
β’ ((π β {π}) β V β ((π β {π}) β π« (Baseβπ) β (π β {π}) β (Baseβπ))) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ (π β π«
(Baseβπ) β
((π β {π}) β π«
(Baseβπ) β
(π β {π}) β (Baseβπ))) |
19 | 15, 18 | mpbird 256 |
. . . . . 6
β’ (π β π«
(Baseβπ) β
(π β {π}) β π«
(Baseβπ)) |
20 | | lincresunit.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
21 | 20 | pweqi 4576 |
. . . . . 6
β’ π«
π΅ = π«
(Baseβπ) |
22 | 19, 21 | eleq2s 2855 |
. . . . 5
β’ (π β π« π΅ β (π β {π}) β π« (Baseβπ)) |
23 | 22 | 3ad2ant1 1133 |
. . . 4
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (π β {π}) β π« (Baseβπ)) |
24 | 23 | adantr 481 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π β {π}) β π« (Baseβπ)) |
25 | | lincval 46480 |
. . 3
β’ ((π β LMod β§ (πΉ βΎ (π β {π})) β ((Baseβ(Scalarβπ)) βm (π β {π})) β§ (π β {π}) β π« (Baseβπ)) β ((πΉ βΎ (π β {π}))( linC βπ)(π β {π})) = (π Ξ£g (π§ β (π β {π}) β¦ (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§)))) |
26 | 1, 13, 24, 25 | syl3anc 1371 |
. 2
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β ((πΉ βΎ (π β {π}))( linC βπ)(π β {π})) = (π Ξ£g (π§ β (π β {π}) β¦ (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§)))) |
27 | | simpll 765 |
. . . . . 6
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β (π β π« π΅ β§ π β LMod β§ π β π)) |
28 | | simplr1 1215 |
. . . . . 6
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β πΉ β (πΈ βm π)) |
29 | | simplr2 1216 |
. . . . . 6
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β (πΉβπ) β π) |
30 | | simpr 485 |
. . . . . 6
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β π§ β (π β {π})) |
31 | | lincresunit.u |
. . . . . . 7
β’ π = (Unitβπ
) |
32 | | lincresunit.0 |
. . . . . . 7
β’ 0 =
(0gβπ
) |
33 | | lincresunit.z |
. . . . . . 7
β’ π = (0gβπ) |
34 | | lincresunit.n |
. . . . . . 7
β’ π = (invgβπ
) |
35 | | lincresunit.i |
. . . . . . 7
β’ πΌ = (invrβπ
) |
36 | | lincresunit.t |
. . . . . . 7
β’ Β· =
(.rβπ
) |
37 | | lincresunit.g |
. . . . . . 7
β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) |
38 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit3lem1 46550 |
. . . . . 6
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ π§ β (π β {π}))) β ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§)) = ((πΉβπ§)( Β·π
βπ)π§)) |
39 | 27, 28, 29, 30, 38 | syl13anc 1372 |
. . . . 5
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§)) = ((πΉβπ§)( Β·π
βπ)π§)) |
40 | | fvres 6861 |
. . . . . . . 8
β’ (π§ β (π β {π}) β ((πΉ βΎ (π β {π}))βπ§) = (πΉβπ§)) |
41 | 40 | adantl 482 |
. . . . . . 7
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β ((πΉ βΎ (π β {π}))βπ§) = (πΉβπ§)) |
42 | 41 | eqcomd 2742 |
. . . . . 6
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β (πΉβπ§) = ((πΉ βΎ (π β {π}))βπ§)) |
43 | 42 | oveq1d 7372 |
. . . . 5
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β ((πΉβπ§)( Β·π
βπ)π§) = (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§)) |
44 | 39, 43 | eqtrd 2776 |
. . . 4
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§)) = (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§)) |
45 | 44 | mpteq2dva 5205 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π§ β (π β {π}) β¦ ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§))) = (π§ β (π β {π}) β¦ (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§))) |
46 | 45 | oveq2d 7373 |
. 2
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π Ξ£g
(π§ β (π β {π}) β¦ ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§)))) = (π Ξ£g (π§ β (π β {π}) β¦ (((πΉ βΎ (π β {π}))βπ§)( Β·π
βπ)π§)))) |
47 | | eqid 2736 |
. . 3
β’
(+gβπ) = (+gβπ) |
48 | | eqid 2736 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
49 | | difexg 5284 |
. . . . 5
β’ (π β π« π΅ β (π β {π}) β V) |
50 | 49 | 3ad2ant1 1133 |
. . . 4
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (π β {π}) β V) |
51 | 50 | adantr 481 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π β {π}) β V) |
52 | 3 | lmodfgrp 20331 |
. . . . . . 7
β’ (π β LMod β π
β Grp) |
53 | 52 | 3ad2ant2 1134 |
. . . . . 6
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β π
β Grp) |
54 | 53 | adantr 481 |
. . . . 5
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ πΉ β (πΈ βm π)) β π
β Grp) |
55 | | elmapi 8787 |
. . . . . . 7
β’ (πΉ β (πΈ βm π) β πΉ:πβΆπΈ) |
56 | | ffvelcdm 7032 |
. . . . . . . . 9
β’ ((πΉ:πβΆπΈ β§ π β π) β (πΉβπ) β πΈ) |
57 | 56 | expcom 414 |
. . . . . . . 8
β’ (π β π β (πΉ:πβΆπΈ β (πΉβπ) β πΈ)) |
58 | 57 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (πΉ:πβΆπΈ β (πΉβπ) β πΈ)) |
59 | 55, 58 | syl5com 31 |
. . . . . 6
β’ (πΉ β (πΈ βm π) β ((π β π« π΅ β§ π β LMod β§ π β π) β (πΉβπ) β πΈ)) |
60 | 59 | impcom 408 |
. . . . 5
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ πΉ β (πΈ βm π)) β (πΉβπ) β πΈ) |
61 | 2, 34 | grpinvcl 18798 |
. . . . 5
β’ ((π
β Grp β§ (πΉβπ) β πΈ) β (πβ(πΉβπ)) β πΈ) |
62 | 54, 60, 61 | syl2anc 584 |
. . . 4
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ πΉ β (πΈ βm π)) β (πβ(πΉβπ)) β πΈ) |
63 | 62 | 3ad2antr1 1188 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (πβ(πΉβπ)) β πΈ) |
64 | 1 | adantr 481 |
. . . 4
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β π β LMod) |
65 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit1 46548 |
. . . . . . 7
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β πΊ β (πΈ βm (π β {π}))) |
66 | 65 | 3adantr3 1171 |
. . . . . 6
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΊ β (πΈ βm (π β {π}))) |
67 | | elmapi 8787 |
. . . . . 6
β’ (πΊ β (πΈ βm (π β {π})) β πΊ:(π β {π})βΆπΈ) |
68 | | ffvelcdm 7032 |
. . . . . . 7
β’ ((πΊ:(π β {π})βΆπΈ β§ π§ β (π β {π})) β (πΊβπ§) β πΈ) |
69 | 68 | ex 413 |
. . . . . 6
β’ (πΊ:(π β {π})βΆπΈ β (π§ β (π β {π}) β (πΊβπ§) β πΈ)) |
70 | 66, 67, 69 | 3syl 18 |
. . . . 5
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π§ β (π β {π}) β (πΊβπ§) β πΈ)) |
71 | 70 | imp 407 |
. . . 4
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β (πΊβπ§) β πΈ) |
72 | | elpwi 4567 |
. . . . . . . 8
β’ (π β π« π΅ β π β π΅) |
73 | | eldifi 4086 |
. . . . . . . . 9
β’ (π§ β (π β {π}) β π§ β π) |
74 | | ssel2 3939 |
. . . . . . . . . 10
β’ ((π β π΅ β§ π§ β π) β π§ β π΅) |
75 | 74 | expcom 414 |
. . . . . . . . 9
β’ (π§ β π β (π β π΅ β π§ β π΅)) |
76 | 73, 75 | syl 17 |
. . . . . . . 8
β’ (π§ β (π β {π}) β (π β π΅ β π§ β π΅)) |
77 | 72, 76 | syl5com 31 |
. . . . . . 7
β’ (π β π« π΅ β (π§ β (π β {π}) β π§ β π΅)) |
78 | 77 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (π§ β (π β {π}) β π§ β π΅)) |
79 | 78 | adantr 481 |
. . . . 5
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π§ β (π β {π}) β π§ β π΅)) |
80 | 79 | imp 407 |
. . . 4
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β π§ β π΅) |
81 | 20, 3, 48, 2 | lmodvscl 20339 |
. . . 4
β’ ((π β LMod β§ (πΊβπ§) β πΈ β§ π§ β π΅) β ((πΊβπ§)( Β·π
βπ)π§) β π΅) |
82 | 64, 71, 80, 81 | syl3anc 1371 |
. . 3
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β§ π§ β (π β {π})) β ((πΊβπ§)( Β·π
βπ)π§) β π΅) |
83 | | simp2 1137 |
. . . . . 6
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β π β LMod) |
84 | 83, 23 | jca 512 |
. . . . 5
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (π β LMod β§ (π β {π}) β π« (Baseβπ))) |
85 | 84 | adantr 481 |
. . . 4
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π β LMod β§ (π β {π}) β π« (Baseβπ))) |
86 | 20, 3, 2, 31, 32, 33, 34, 35, 36, 37 | lincresunit2 46549 |
. . . . 5
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΊ finSupp 0 ) |
87 | 86, 32 | breqtrdi 5146 |
. . . 4
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΊ finSupp
(0gβπ
)) |
88 | 3, 2 | scmfsupp 46444 |
. . . . 5
β’ (((π β LMod β§ (π β {π}) β π« (Baseβπ)) β§ πΊ β (πΈ βm (π β {π})) β§ πΊ finSupp (0gβπ
)) β (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π
βπ)π§)) finSupp (0gβπ)) |
89 | 88, 33 | breqtrrdi 5147 |
. . . 4
β’ (((π β LMod β§ (π β {π}) β π« (Baseβπ)) β§ πΊ β (πΈ βm (π β {π})) β§ πΊ finSupp (0gβπ
)) β (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π
βπ)π§)) finSupp π) |
90 | 85, 66, 87, 89 | syl3anc 1371 |
. . 3
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π
βπ)π§)) finSupp π) |
91 | 20, 3, 2, 33, 47, 48, 1, 51, 63, 82, 90 | gsumvsmul 20386 |
. 2
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β (π Ξ£g
(π§ β (π β {π}) β¦ ((πβ(πΉβπ))( Β·π
βπ)((πΊβπ§)( Β·π
βπ)π§)))) = ((πβ(πΉβπ))( Β·π
βπ)(π Ξ£g (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π
βπ)π§))))) |
92 | 26, 46, 91 | 3eqtr2rd 2783 |
1
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β ((πβ(πΉβπ))( Β·π
βπ)(π Ξ£g (π§ β (π β {π}) β¦ ((πΊβπ§)( Β·π
βπ)π§)))) = ((πΉ βΎ (π β {π}))( linC βπ)(π β {π}))) |