Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β LMod) β π β LMod) |
2 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π β LMod) |
3 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π β (Baseβπ)) |
4 | | elpwg 4568 |
. . . . . . . . . . . . . 14
β’ (π β π β (π β π« (Baseβπ) β π β (Baseβπ))) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β π« (Baseβπ) β π β (Baseβπ))) |
6 | 3, 5 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π β π« (Baseβπ)) |
7 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β (Baseβπ) β§ π₯ β π) β π₯ β π) |
8 | 7 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π₯ β π) |
9 | 2, 6, 8 | 3jca 1129 |
. . . . . . . . . . 11
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β LMod β§ π β π« (Baseβπ) β§ π₯ β π)) |
10 | 9 | adantl 483 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π β LMod β§ π β π« (Baseβπ) β§ π₯ β π)) |
11 | | simpl 484 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π β (π΅ βm π) β§ π finSupp 0 )) |
12 | | lindslinind.g |
. . . . . . . . . . 11
β’ πΊ = (π βΎ (π β {π₯})) |
13 | 12 | a1i 11 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β πΊ = (π βΎ (π β {π₯}))) |
14 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
15 | | lindslinind.r |
. . . . . . . . . . 11
β’ π
= (Scalarβπ) |
16 | | lindslinind.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ
) |
17 | | eqid 2737 |
. . . . . . . . . . 11
β’ (
Β·π βπ) = ( Β·π
βπ) |
18 | | eqid 2737 |
. . . . . . . . . . 11
β’
(+gβπ) = (+gβπ) |
19 | | lindslinind.0 |
. . . . . . . . . . 11
β’ 0 =
(0gβπ
) |
20 | 14, 15, 16, 17, 18, 19 | lincdifsn 46579 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π«
(Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 ) β§ πΊ = (π βΎ (π β {π₯}))) β (π( linC βπ)π) = ((πΊ( linC βπ)(π β {π₯}))(+gβπ)((πβπ₯)( Β·π
βπ)π₯))) |
21 | 10, 11, 13, 20 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π( linC βπ)π) = ((πΊ( linC βπ)(π β {π₯}))(+gβπ)((πβπ₯)( Β·π
βπ)π₯))) |
22 | 21 | eqeq1d 2739 |
. . . . . . . 8
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π( linC βπ)π) = π β ((πΊ( linC βπ)(π β {π₯}))(+gβπ)((πβπ₯)( Β·π
βπ)π₯)) = π)) |
23 | | lmodgrp 20345 |
. . . . . . . . . . 11
β’ (π β LMod β π β Grp) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π β§ π β LMod) β π β Grp) |
25 | 24 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π β Grp) |
26 | 1 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π β LMod) |
27 | | elmapi 8794 |
. . . . . . . . . . . . 13
β’ (π β (π΅ βm π) β π:πβΆπ΅) |
28 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
β’ ((π:πβΆπ΅ β§ π₯ β π) β (πβπ₯) β π΅) |
29 | 28 | expcom 415 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β (π:πβΆπ΅ β (πβπ₯) β π΅)) |
30 | 29 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π:πβΆπ΅ β (πβπ₯) β π΅)) |
31 | 27, 30 | syl5com 31 |
. . . . . . . . . . . 12
β’ (π β (π΅ βm π) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (πβπ₯) β π΅)) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (π΅ βm π) β§ π finSupp 0 ) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (πβπ₯) β π΅)) |
33 | 32 | imp 408 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (πβπ₯) β π΅) |
34 | | ssel2 3944 |
. . . . . . . . . . 11
β’ ((π β (Baseβπ) β§ π₯ β π) β π₯ β (Baseβπ)) |
35 | 34 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π₯ β (Baseβπ)) |
36 | 14, 15, 17, 16 | lmodvscl 20355 |
. . . . . . . . . 10
β’ ((π β LMod β§ (πβπ₯) β π΅ β§ π₯ β (Baseβπ)) β ((πβπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
37 | 26, 33, 35, 36 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((πβπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
38 | | difexg 5289 |
. . . . . . . . . . . . 13
β’ (π β π β (π β {π₯}) β V) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β V) |
40 | | ssdifss 4100 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β (π β {π₯}) β (Baseβπ)) |
41 | 40 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β (Baseβπ)) |
42 | 39, 41 | jca 513 |
. . . . . . . . . . 11
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β {π₯}) β V β§ (π β {π₯}) β (Baseβπ))) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π β {π₯}) β V β§ (π β {π₯}) β (Baseβπ))) |
44 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π β π β§ π β LMod)) |
45 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β (Baseβπ) β§ π₯ β π) β π β (Baseβπ)) |
46 | 45 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π β (Baseβπ)) |
47 | 7 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π₯ β π) |
48 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β (π΅ βm π) β§ π finSupp 0 ) β π β (π΅ βm π)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β π β (π΅ βm π)) |
50 | | lindslinind.z |
. . . . . . . . . . . . 13
β’ π = (0gβπ) |
51 | | lindslinind.y |
. . . . . . . . . . . . 13
β’ π = ((invgβπ
)β(πβπ₯)) |
52 | 15, 16, 19, 50, 51, 12 | lindslinindimp2lem2 46614 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π β§ π β (π΅ βm π))) β πΊ β (π΅ βm (π β {π₯}))) |
53 | 44, 46, 47, 49, 52 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β πΊ β (π΅ βm (π β {π₯}))) |
54 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β (Baseβπ) β§ π₯ β π)) |
55 | 54 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π β (Baseβπ) β§ π₯ β π)) |
56 | 15, 16, 19, 50, 51, 12 | lindslinindimp2lem3 46615 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 )) β πΊ finSupp 0 ) |
57 | 44, 55, 11, 56 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β πΊ finSupp 0 ) |
58 | 53, 57 | jca 513 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (πΊ β (π΅ βm (π β {π₯})) β§ πΊ finSupp 0 )) |
59 | 14, 15, 16, 19 | lincfsuppcl 46568 |
. . . . . . . . . 10
β’ ((π β LMod β§ ((π β {π₯}) β V β§ (π β {π₯}) β (Baseβπ)) β§ (πΊ β (π΅ βm (π β {π₯})) β§ πΊ finSupp 0 )) β (πΊ( linC βπ)(π β {π₯})) β (Baseβπ)) |
60 | 26, 43, 58, 59 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (πΊ( linC βπ)(π β {π₯})) β (Baseβπ)) |
61 | | eqid 2737 |
. . . . . . . . . 10
β’
(invgβπ) = (invgβπ) |
62 | 14, 18, 50, 61 | grpinvid2 18810 |
. . . . . . . . 9
β’ ((π β Grp β§ ((πβπ₯)( Β·π
βπ)π₯) β (Baseβπ) β§ (πΊ( linC βπ)(π β {π₯})) β (Baseβπ)) β (((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (πΊ( linC βπ)(π β {π₯})) β ((πΊ( linC βπ)(π β {π₯}))(+gβπ)((πβπ₯)( Β·π
βπ)π₯)) = π)) |
63 | 25, 37, 60, 62 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (πΊ( linC βπ)(π β {π₯})) β ((πΊ( linC βπ)(π β {π₯}))(+gβπ)((πβπ₯)( Β·π
βπ)π₯)) = π)) |
64 | 22, 63 | bitr4d 282 |
. . . . . . 7
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π( linC βπ)π) = π β ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (πΊ( linC βπ)(π β {π₯})))) |
65 | | eqcom 2744 |
. . . . . . . 8
β’
(((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (πΊ( linC βπ)(π β {π₯})) β (πΊ( linC βπ)(π β {π₯})) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯))) |
66 | 15 | fveq2i 6850 |
. . . . . . . . . . . . . 14
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
67 | 16, 66 | eqtri 2765 |
. . . . . . . . . . . . 13
β’ π΅ =
(Baseβ(Scalarβπ)) |
68 | 67 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ (π΅ βm (π β {π₯})) = ((Baseβ(Scalarβπ)) βm (π β {π₯})) |
69 | 53, 68 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β πΊ β ((Baseβ(Scalarβπ)) βm (π β {π₯}))) |
70 | 39, 41 | elpwd 4571 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β π« (Baseβπ)) |
71 | 70 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π β {π₯}) β π« (Baseβπ)) |
72 | | lincval 46564 |
. . . . . . . . . . 11
β’ ((π β LMod β§ πΊ β
((Baseβ(Scalarβπ)) βm (π β {π₯})) β§ (π β {π₯}) β π« (Baseβπ)) β (πΊ( linC βπ)(π β {π₯})) = (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦)))) |
73 | 26, 69, 71, 72 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (πΊ( linC βπ)(π β {π₯})) = (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦)))) |
74 | 73 | eqeq1d 2739 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((πΊ( linC βπ)(π β {π₯})) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦))) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)))) |
75 | 12 | fveq1i 6848 |
. . . . . . . . . . . . . . . 16
β’ (πΊβπ¦) = ((π βΎ (π β {π₯}))βπ¦) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β§ π¦ β (π β {π₯})) β (πΊβπ¦) = ((π βΎ (π β {π₯}))βπ¦)) |
77 | | fvres 6866 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (π β {π₯}) β ((π βΎ (π β {π₯}))βπ¦) = (πβπ¦)) |
78 | 77 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β§ π¦ β (π β {π₯})) β ((π βΎ (π β {π₯}))βπ¦) = (πβπ¦)) |
79 | 76, 78 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β§ π¦ β (π β {π₯})) β (πΊβπ¦) = (πβπ¦)) |
80 | 79 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β§ π¦ β (π β {π₯})) β ((πΊβπ¦)( Β·π
βπ)π¦) = ((πβπ¦)( Β·π
βπ)π¦)) |
81 | 80 | mpteq2dva 5210 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦)) = (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) |
82 | 81 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦))) = (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦)))) |
83 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(invgβπ
) = (invgβπ
) |
84 | 14, 15, 17, 61, 16, 83, 26, 35, 33 | lmodvsneg 20382 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯)) |
85 | 51 | eqcomi 2746 |
. . . . . . . . . . . . . 14
β’
((invgβπ
)β(πβπ₯)) = π |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((invgβπ
)β(πβπ₯)) = π) |
87 | 86 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( Β·π
βπ)π₯)) |
88 | 84, 87 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (π( Β·π
βπ)π₯)) |
89 | 82, 88 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦))) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
90 | 89 | biimpd 228 |
. . . . . . . . 9
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π Ξ£g (π¦ β (π β {π₯}) β¦ ((πΊβπ¦)( Β·π
βπ)π¦))) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
91 | 74, 90 | sylbid 239 |
. . . . . . . 8
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((πΊ( linC βπ)(π β {π₯})) = ((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
92 | 65, 91 | biimtrid 241 |
. . . . . . 7
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β (((invgβπ)β((πβπ₯)( Β·π
βπ)π₯)) = (πΊ( linC βπ)(π β {π₯})) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
93 | 64, 92 | sylbid 239 |
. . . . . 6
β’ (((π β (π΅ βm π) β§ π finSupp 0 ) β§ ((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π))) β ((π( linC βπ)π) = π β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
94 | 93 | ex 414 |
. . . . 5
β’ ((π β (π΅ βm π) β§ π finSupp 0 ) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π( linC βπ)π) = π β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯)))) |
95 | 94 | com23 86 |
. . . 4
β’ ((π β (π΅ βm π) β§ π finSupp 0 ) β ((π( linC βπ)π) = π β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯)))) |
96 | 95 | 3impia 1118 |
. . 3
β’ ((π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
97 | 96 | com12 32 |
. 2
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯))) |
98 | 97 | 3impia 1118 |
1
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) β (π Ξ£g (π¦ β (π β {π₯}) β¦ ((πβπ¦)( Β·π
βπ)π¦))) = (π( Β·π
βπ)π₯)) |