Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2737 |
. . 3
β’
(0gβπ) = (0gβπ) |
3 | | lincsum.p |
. . 3
β’ + =
(+gβπ) |
4 | | lmodcmn 20386 |
. . . . 5
β’ (π β LMod β π β CMnd) |
5 | 4 | adantr 482 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β
CMnd) |
6 | 5 | 3ad2ant1 1134 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β π β CMnd) |
7 | | simpr 486 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β π«
(Baseβπ)) |
8 | 7 | 3ad2ant1 1134 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β π β π« (Baseβπ)) |
9 | | simpl 484 |
. . . . . 6
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β
LMod) |
10 | 9 | 3ad2ant1 1134 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β π β LMod) |
11 | 10 | adantr 482 |
. . . 4
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β π β LMod) |
12 | | elmapi 8794 |
. . . . . . . 8
β’ (π΄ β (π
βm π) β π΄:πβΆπ
) |
13 | | ffvelcdm 7037 |
. . . . . . . . 9
β’ ((π΄:πβΆπ
β§ π₯ β π) β (π΄βπ₯) β π
) |
14 | 13 | ex 414 |
. . . . . . . 8
β’ (π΄:πβΆπ
β (π₯ β π β (π΄βπ₯) β π
)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
β’ (π΄ β (π
βm π) β (π₯ β π β (π΄βπ₯) β π
)) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π΄ β (π
βm π) β§ π΅ β (π
βm π)) β (π₯ β π β (π΄βπ₯) β π
)) |
17 | 16 | 3ad2ant2 1135 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β (π΄βπ₯) β π
)) |
18 | 17 | imp 408 |
. . . 4
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β (π΄βπ₯) β π
) |
19 | | elelpwi 4575 |
. . . . . . . 8
β’ ((π₯ β π β§ π β π« (Baseβπ)) β π₯ β (Baseβπ)) |
20 | 19 | expcom 415 |
. . . . . . 7
β’ (π β π«
(Baseβπ) β
(π₯ β π β π₯ β (Baseβπ))) |
21 | 20 | adantl 483 |
. . . . . 6
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π₯ β π β π₯ β (Baseβπ))) |
22 | 21 | 3ad2ant1 1134 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β π₯ β (Baseβπ))) |
23 | 22 | imp 408 |
. . . 4
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β π₯ β (Baseβπ)) |
24 | | lincsum.s |
. . . . 5
β’ π = (Scalarβπ) |
25 | | eqid 2737 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
26 | | lincsum.r |
. . . . 5
β’ π
= (Baseβπ) |
27 | 1, 24, 25, 26 | lmodvscl 20355 |
. . . 4
β’ ((π β LMod β§ (π΄βπ₯) β π
β§ π₯ β (Baseβπ)) β ((π΄βπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
28 | 11, 18, 23, 27 | syl3anc 1372 |
. . 3
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β ((π΄βπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
29 | | elmapi 8794 |
. . . . . . . 8
β’ (π΅ β (π
βm π) β π΅:πβΆπ
) |
30 | | ffvelcdm 7037 |
. . . . . . . . 9
β’ ((π΅:πβΆπ
β§ π₯ β π) β (π΅βπ₯) β π
) |
31 | 30 | ex 414 |
. . . . . . . 8
β’ (π΅:πβΆπ
β (π₯ β π β (π΅βπ₯) β π
)) |
32 | 29, 31 | syl 17 |
. . . . . . 7
β’ (π΅ β (π
βm π) β (π₯ β π β (π΅βπ₯) β π
)) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((π΄ β (π
βm π) β§ π΅ β (π
βm π)) β (π₯ β π β (π΅βπ₯) β π
)) |
34 | 33 | 3ad2ant2 1135 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β (π΅βπ₯) β π
)) |
35 | 34 | imp 408 |
. . . 4
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β (π΅βπ₯) β π
) |
36 | 1, 24, 25, 26 | lmodvscl 20355 |
. . . 4
β’ ((π β LMod β§ (π΅βπ₯) β π
β§ π₯ β (Baseβπ)) β ((π΅βπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
37 | 11, 35, 23, 36 | syl3anc 1372 |
. . 3
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β§ π₯ β π) β ((π΅βπ₯)( Β·π
βπ)π₯) β (Baseβπ)) |
38 | | eqidd 2738 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯)) = (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯))) |
39 | | eqidd 2738 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯)) = (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯))) |
40 | | id 22 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π β LMod β§ π β π«
(Baseβπ))) |
41 | | simpl 484 |
. . . 4
β’ ((π΄ β (π
βm π) β§ π΅ β (π
βm π)) β π΄ β (π
βm π)) |
42 | | simpl 484 |
. . . 4
β’ ((π΄ finSupp
(0gβπ)
β§ π΅ finSupp
(0gβπ))
β π΄ finSupp
(0gβπ)) |
43 | 24, 26 | scmfsupp 46528 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π΄ β (π
βm π) β§ π΄ finSupp (0gβπ)) β (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
44 | 40, 41, 42, 43 | syl3an 1161 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
45 | | simpr 486 |
. . . 4
β’ ((π΄ β (π
βm π) β§ π΅ β (π
βm π)) β π΅ β (π
βm π)) |
46 | | simpr 486 |
. . . 4
β’ ((π΄ finSupp
(0gβπ)
β§ π΅ finSupp
(0gβπ))
β π΅ finSupp
(0gβπ)) |
47 | 24, 26 | scmfsupp 46528 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π΅ β (π
βm π) β§ π΅ finSupp (0gβπ)) β (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
48 | 40, 45, 46, 47 | syl3an 1161 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 19708 |
. 2
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π Ξ£g (π₯ β π β¦ (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯)))) = ((π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯))) + (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯))))) |
50 | 7 | adantr 482 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π β π« (Baseβπ)) |
51 | | elmapfn 8810 |
. . . . . . . 8
β’ (π΄ β (π
βm π) β π΄ Fn π) |
52 | 51 | ad2antrl 727 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π΄ Fn π) |
53 | | elmapfn 8810 |
. . . . . . . 8
β’ (π΅ β (π
βm π) β π΅ Fn π) |
54 | 53 | ad2antll 728 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π΅ Fn π) |
55 | 50, 52, 54 | offvalfv 46492 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π΄ βf β π΅) = (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦)))) |
56 | 55 | 3adant3 1133 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π΄ βf β π΅) = (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦)))) |
57 | 24 | lmodfgrp 20347 |
. . . . . . . . . . 11
β’ (π β LMod β π β Grp) |
58 | 57 | grpmndd 18767 |
. . . . . . . . . 10
β’ (π β LMod β π β Mnd) |
59 | 58 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π¦ β π) β π β Mnd) |
60 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((π΄:πβΆπ
β§ π¦ β π) β (π΄βπ¦) β π
) |
61 | 60 | ex 414 |
. . . . . . . . . . . . 13
β’ (π΄:πβΆπ
β (π¦ β π β (π΄βπ¦) β π
)) |
62 | 12, 61 | syl 17 |
. . . . . . . . . . . 12
β’ (π΄ β (π
βm π) β (π¦ β π β (π΄βπ¦) β π
)) |
63 | 62 | ad2antrl 727 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π¦ β π β (π΄βπ¦) β π
)) |
64 | 63 | imp 408 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π¦ β π) β (π΄βπ¦) β π
) |
65 | 24 | fveq2i 6850 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβ(Scalarβπ)) |
66 | 26, 65 | eqtri 2765 |
. . . . . . . . . 10
β’ π
=
(Baseβ(Scalarβπ)) |
67 | 64, 66 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π¦ β π) β (π΄βπ¦) β (Baseβ(Scalarβπ))) |
68 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((π΅:πβΆπ
β§ π¦ β π) β (π΅βπ¦) β π
) |
69 | 68, 66 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
β’ ((π΅:πβΆπ
β§ π¦ β π) β (π΅βπ¦) β (Baseβ(Scalarβπ))) |
70 | 69 | ex 414 |
. . . . . . . . . . . 12
β’ (π΅:πβΆπ
β (π¦ β π β (π΅βπ¦) β (Baseβ(Scalarβπ)))) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . 11
β’ (π΅ β (π
βm π) β (π¦ β π β (π΅βπ¦) β (Baseβ(Scalarβπ)))) |
72 | 71 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π¦ β π β (π΅βπ¦) β (Baseβ(Scalarβπ)))) |
73 | 72 | imp 408 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π¦ β π) β (π΅βπ¦) β (Baseβ(Scalarβπ))) |
74 | 24 | eqcomi 2746 |
. . . . . . . . . . 11
β’
(Scalarβπ) =
π |
75 | 74 | fveq2i 6850 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβπ)) = (Baseβπ) |
76 | | lincsum.b |
. . . . . . . . . 10
β’ β =
(+gβπ) |
77 | 75, 76 | mndcl 18571 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π΄βπ¦) β (Baseβ(Scalarβπ)) β§ (π΅βπ¦) β (Baseβ(Scalarβπ))) β ((π΄βπ¦) β (π΅βπ¦)) β (Baseβ(Scalarβπ))) |
78 | 59, 67, 73, 77 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π¦ β π) β ((π΄βπ¦) β (π΅βπ¦)) β (Baseβ(Scalarβπ))) |
79 | 78 | fmpttd 7068 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))):πβΆ(Baseβ(Scalarβπ))) |
80 | | fvex 6860 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) β V |
81 | | elmapg 8785 |
. . . . . . . 8
β’
(((Baseβ(Scalarβπ)) β V β§ π β π« (Baseβπ)) β ((π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))) β ((Baseβ(Scalarβπ)) βm π) β (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))):πβΆ(Baseβ(Scalarβπ)))) |
82 | 80, 50, 81 | sylancr 588 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β ((π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))) β ((Baseβ(Scalarβπ)) βm π) β (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))):πβΆ(Baseβ(Scalarβπ)))) |
83 | 79, 82 | mpbird 257 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))) β ((Baseβ(Scalarβπ)) βm π)) |
84 | 83 | 3adant3 1133 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π¦ β π β¦ ((π΄βπ¦) β (π΅βπ¦))) β ((Baseβ(Scalarβπ)) βm π)) |
85 | 56, 84 | eqeltrd 2838 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π΄ βf β π΅) β ((Baseβ(Scalarβπ)) βm π)) |
86 | | lincval 46564 |
. . . 4
β’ ((π β LMod β§ (π΄ βf β π΅) β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β ((π΄ βf β π΅)( linC βπ)π) = (π Ξ£g (π₯ β π β¦ (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯)))) |
87 | 10, 85, 8, 86 | syl3anc 1372 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β ((π΄ βf β π΅)( linC βπ)π) = (π Ξ£g (π₯ β π β¦ (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯)))) |
88 | 51, 53 | anim12i 614 |
. . . . . . . . . . . 12
β’ ((π΄ β (π
βm π) β§ π΅ β (π
βm π)) β (π΄ Fn π β§ π΅ Fn π)) |
89 | 88 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π΄ Fn π β§ π΅ Fn π)) |
90 | 89 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (π΄ Fn π β§ π΅ Fn π)) |
91 | 50 | anim1i 616 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (π β π« (Baseβπ) β§ π₯ β π)) |
92 | | fnfvof 7639 |
. . . . . . . . . 10
β’ (((π΄ Fn π β§ π΅ Fn π) β§ (π β π« (Baseβπ) β§ π₯ β π)) β ((π΄ βf β π΅)βπ₯) = ((π΄βπ₯) β (π΅βπ₯))) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β ((π΄ βf β π΅)βπ₯) = ((π΄βπ₯) β (π΅βπ₯))) |
94 | 76 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β β =
(+gβπ)) |
95 | 94 | oveqd 7379 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β ((π΄βπ₯) β (π΅βπ₯)) = ((π΄βπ₯)(+gβπ)(π΅βπ₯))) |
96 | 93, 95 | eqtrd 2777 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β ((π΄ βf β π΅)βπ₯) = ((π΄βπ₯)(+gβπ)(π΅βπ₯))) |
97 | 96 | oveq1d 7377 |
. . . . . . 7
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯) = (((π΄βπ₯)(+gβπ)(π΅βπ₯))( Β·π
βπ)π₯)) |
98 | 9 | adantr 482 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π β LMod) |
99 | 98 | adantr 482 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β π β LMod) |
100 | 15 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π₯ β π β (π΄βπ₯) β π
)) |
101 | 100 | imp 408 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (π΄βπ₯) β π
) |
102 | 32 | ad2antll 728 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π₯ β π β (π΅βπ₯) β π
)) |
103 | 102 | imp 408 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (π΅βπ₯) β π
) |
104 | 21 | adantr 482 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π₯ β π β π₯ β (Baseβπ))) |
105 | 104 | imp 408 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β π₯ β (Baseβπ)) |
106 | | eqid 2737 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
107 | 24 | fveq2i 6850 |
. . . . . . . . 9
β’
(+gβπ) = (+gβ(Scalarβπ)) |
108 | 1, 3, 106, 25, 66, 107 | lmodvsdir 20362 |
. . . . . . . 8
β’ ((π β LMod β§ ((π΄βπ₯) β π
β§ (π΅βπ₯) β π
β§ π₯ β (Baseβπ))) β (((π΄βπ₯)(+gβπ)(π΅βπ₯))( Β·π
βπ)π₯) = (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))) |
109 | 99, 101, 103, 105, 108 | syl13anc 1373 |
. . . . . . 7
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (((π΄βπ₯)(+gβπ)(π΅βπ₯))( Β·π
βπ)π₯) = (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))) |
110 | 97, 109 | eqtrd 2777 |
. . . . . 6
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β§ π₯ β π) β (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯) = (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))) |
111 | 110 | mpteq2dva 5210 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π₯ β π β¦ (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯)) = (π₯ β π β¦ (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯)))) |
112 | 111 | oveq2d 7378 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π Ξ£g (π₯ β π β¦ (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯))) = (π Ξ£g (π₯ β π β¦ (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))))) |
113 | 112 | 3adant3 1133 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π Ξ£g (π₯ β π β¦ (((π΄ βf β π΅)βπ₯)( Β·π
βπ)π₯))) = (π Ξ£g (π₯ β π β¦ (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))))) |
114 | 87, 113 | eqtrd 2777 |
. 2
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β ((π΄ βf β π΅)( linC βπ)π) = (π Ξ£g (π₯ β π β¦ (((π΄βπ₯)( Β·π
βπ)π₯) + ((π΅βπ₯)( Β·π
βπ)π₯))))) |
115 | | lincsum.x |
. . . 4
β’ π = (π΄( linC βπ)π) |
116 | | lincsum.y |
. . . 4
β’ π = (π΅( linC βπ)π) |
117 | 115, 116 | oveq12i 7374 |
. . 3
β’ (π + π) = ((π΄( linC βπ)π) + (π΅( linC βπ)π)) |
118 | 66 | oveq1i 7372 |
. . . . . . . . 9
β’ (π
βm π) =
((Baseβ(Scalarβπ)) βm π) |
119 | 118 | eleq2i 2830 |
. . . . . . . 8
β’ (π΄ β (π
βm π) β π΄ β ((Baseβ(Scalarβπ)) βm π)) |
120 | 119 | biimpi 215 |
. . . . . . 7
β’ (π΄ β (π
βm π) β π΄ β ((Baseβ(Scalarβπ)) βm π)) |
121 | 120 | ad2antrl 727 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π΄ β ((Baseβ(Scalarβπ)) βm π)) |
122 | | lincval 46564 |
. . . . . 6
β’ ((π β LMod β§ π΄ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π΄( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯)))) |
123 | 98, 121, 50, 122 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π΄( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯)))) |
124 | 118 | eleq2i 2830 |
. . . . . . . 8
β’ (π΅ β (π
βm π) β π΅ β ((Baseβ(Scalarβπ)) βm π)) |
125 | 124 | biimpi 215 |
. . . . . . 7
β’ (π΅ β (π
βm π) β π΅ β ((Baseβ(Scalarβπ)) βm π)) |
126 | 125 | ad2antll 728 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β π΅ β ((Baseβ(Scalarβπ)) βm π)) |
127 | | lincval 46564 |
. . . . . 6
β’ ((π β LMod β§ π΅ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π΅( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯)))) |
128 | 98, 126, 50, 127 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β (π΅( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯)))) |
129 | 123, 128 | oveq12d 7380 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π))) β ((π΄( linC βπ)π) + (π΅( linC βπ)π)) = ((π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯))) + (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯))))) |
130 | 129 | 3adant3 1133 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β ((π΄( linC βπ)π) + (π΅( linC βπ)π)) = ((π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯))) + (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯))))) |
131 | 117, 130 | eqtrid 2789 |
. 2
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π + π) = ((π Ξ£g (π₯ β π β¦ ((π΄βπ₯)( Β·π
βπ)π₯))) + (π Ξ£g (π₯ β π β¦ ((π΅βπ₯)( Β·π
βπ)π₯))))) |
132 | 49, 114, 131 | 3eqtr4rd 2788 |
1
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π΄ β (π
βm π) β§ π΅ β (π
βm π)) β§ (π΄ finSupp (0gβπ) β§ π΅ finSupp (0gβπ))) β (π + π) = ((π΄ βf β π΅)( linC βπ)π)) |