Step | Hyp | Ref
| Expression |
1 | | eldprdi.1 |
. . . . 5
β’ (π β πΊdom DProd π) |
2 | | eldprdi.2 |
. . . . 5
β’ (π β dom π = πΌ) |
3 | 1, 2 | dprddomcld 19788 |
. . . 4
β’ (π β πΌ β V) |
4 | | eldprdi.w |
. . . . 5
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
5 | | eldprdi.3 |
. . . . 5
β’ (π β πΉ β π) |
6 | 4, 1, 2, 5 | dprdfcl 19800 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) β (πβπ₯)) |
7 | | dprdfadd.4 |
. . . . 5
β’ (π β π» β π) |
8 | 4, 1, 2, 7 | dprdfcl 19800 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (π»βπ₯) β (πβπ₯)) |
9 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
10 | 4, 1, 2, 5, 9 | dprdff 19799 |
. . . . 5
β’ (π β πΉ:πΌβΆ(BaseβπΊ)) |
11 | 10 | feqmptd 6914 |
. . . 4
β’ (π β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
12 | 4, 1, 2, 7, 9 | dprdff 19799 |
. . . . 5
β’ (π β π»:πΌβΆ(BaseβπΊ)) |
13 | 12 | feqmptd 6914 |
. . . 4
β’ (π β π» = (π₯ β πΌ β¦ (π»βπ₯))) |
14 | 3, 6, 8, 11, 13 | offval2 7641 |
. . 3
β’ (π β (πΉ βf + π») = (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯)))) |
15 | 1, 2 | dprdf2 19794 |
. . . . . 6
β’ (π β π:πΌβΆ(SubGrpβπΊ)) |
16 | 15 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πβπ₯) β (SubGrpβπΊ)) |
17 | | dprdfadd.b |
. . . . . 6
β’ + =
(+gβπΊ) |
18 | 17 | subgcl 18946 |
. . . . 5
β’ (((πβπ₯) β (SubGrpβπΊ) β§ (πΉβπ₯) β (πβπ₯) β§ (π»βπ₯) β (πβπ₯)) β ((πΉβπ₯) + (π»βπ₯)) β (πβπ₯)) |
19 | 16, 6, 8, 18 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πΉβπ₯) + (π»βπ₯)) β (πβπ₯)) |
20 | 4, 1, 2, 5 | dprdffsupp 19801 |
. . . . . . 7
β’ (π β πΉ finSupp 0 ) |
21 | 4, 1, 2, 7 | dprdffsupp 19801 |
. . . . . . 7
β’ (π β π» finSupp 0 ) |
22 | 20, 21 | fsuppunfi 9333 |
. . . . . 6
β’ (π β ((πΉ supp 0 ) βͺ (π» supp 0 )) β
Fin) |
23 | | ssun1 4136 |
. . . . . . . . . . 11
β’ (πΉ supp 0 ) β ((πΉ supp 0 ) βͺ (π» supp 0 )) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
β’ (π β (πΉ supp 0 ) β ((πΉ supp 0 ) βͺ (π» supp 0 ))) |
25 | | eldprdi.0 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπΊ) |
26 | 25 | fvexi 6860 |
. . . . . . . . . . 11
β’ 0 β
V |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ (π β 0 β V) |
28 | 10, 24, 3, 27 | suppssr 8131 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β ((πΉ supp 0 ) βͺ (π» supp 0 )))) β (πΉβπ₯) = 0 ) |
29 | | ssun2 4137 |
. . . . . . . . . . 11
β’ (π» supp 0 ) β ((πΉ supp 0 ) βͺ (π» supp 0 )) |
30 | 29 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π» supp 0 ) β ((πΉ supp 0 ) βͺ (π» supp 0 ))) |
31 | 12, 30, 3, 27 | suppssr 8131 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΌ β ((πΉ supp 0 ) βͺ (π» supp 0 )))) β (π»βπ₯) = 0 ) |
32 | 28, 31 | oveq12d 7379 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β ((πΉ supp 0 ) βͺ (π» supp 0 )))) β ((πΉβπ₯) + (π»βπ₯)) = ( 0 + 0 )) |
33 | | dprdgrp 19792 |
. . . . . . . . . . 11
β’ (πΊdom DProd π β πΊ β Grp) |
34 | 1, 33 | syl 17 |
. . . . . . . . . 10
β’ (π β πΊ β Grp) |
35 | 9, 25 | grpidcl 18786 |
. . . . . . . . . 10
β’ (πΊ β Grp β 0 β
(BaseβπΊ)) |
36 | 9, 17, 25 | grplid 18788 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ 0 β
(BaseβπΊ)) β (
0 + 0 ) = 0
) |
37 | 34, 35, 36 | syl2anc2 586 |
. . . . . . . . 9
β’ (π β ( 0 + 0 ) = 0 ) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β ((πΉ supp 0 ) βͺ (π» supp 0 )))) β ( 0 + 0 ) = 0
) |
39 | 32, 38 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β ((πΉ supp 0 ) βͺ (π» supp 0 )))) β ((πΉβπ₯) + (π»βπ₯)) = 0 ) |
40 | 39, 3 | suppss2 8135 |
. . . . . 6
β’ (π β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) supp 0 ) β ((πΉ supp 0 ) βͺ (π» supp 0 ))) |
41 | 22, 40 | ssfid 9217 |
. . . . 5
β’ (π β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) supp 0 ) β
Fin) |
42 | | funmpt 6543 |
. . . . . . 7
β’ Fun
(π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) |
43 | 42 | a1i 11 |
. . . . . 6
β’ (π β Fun (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯)))) |
44 | 3 | mptexd 7178 |
. . . . . 6
β’ (π β (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) β V) |
45 | | funisfsupp 9317 |
. . . . . 6
β’ ((Fun
(π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) β§ (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) β V β§ 0 β V) β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) finSupp 0 β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) supp 0 ) β
Fin)) |
46 | 43, 44, 27, 45 | syl3anc 1372 |
. . . . 5
β’ (π β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) finSupp 0 β ((π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) supp 0 ) β
Fin)) |
47 | 41, 46 | mpbird 257 |
. . . 4
β’ (π β (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) finSupp 0 ) |
48 | 4, 1, 2, 19, 47 | dprdwd 19798 |
. . 3
β’ (π β (π₯ β πΌ β¦ ((πΉβπ₯) + (π»βπ₯))) β π) |
49 | 14, 48 | eqeltrd 2834 |
. 2
β’ (π β (πΉ βf + π») β π) |
50 | | eqid 2733 |
. . 3
β’
(CntzβπΊ) =
(CntzβπΊ) |
51 | 34 | grpmndd 18768 |
. . 3
β’ (π β πΊ β Mnd) |
52 | | eqid 2733 |
. . 3
β’ ((πΉ βͺ π») supp 0 ) = ((πΉ βͺ π») supp 0 ) |
53 | 4, 1, 2, 5, 50 | dprdfcntz 19802 |
. . 3
β’ (π β ran πΉ β ((CntzβπΊ)βran πΉ)) |
54 | 4, 1, 2, 7, 50 | dprdfcntz 19802 |
. . 3
β’ (π β ran π» β ((CntzβπΊ)βran π»)) |
55 | 4, 1, 2, 49, 50 | dprdfcntz 19802 |
. . 3
β’ (π β ran (πΉ βf + π») β ((CntzβπΊ)βran (πΉ βf + π»))) |
56 | 51 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β πΊ β Mnd) |
57 | | vex 3451 |
. . . . . . . 8
β’ π₯ β V |
58 | 57 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β π₯ β V) |
59 | | eldifi 4090 |
. . . . . . . . . . 11
β’ (π β (πΌ β π₯) β π β πΌ) |
60 | 59 | adantl 483 |
. . . . . . . . . 10
β’ ((π₯ β πΌ β§ π β (πΌ β π₯)) β π β πΌ) |
61 | | ffvelcdm 7036 |
. . . . . . . . . 10
β’ ((πΉ:πΌβΆ(BaseβπΊ) β§ π β πΌ) β (πΉβπ) β (BaseβπΊ)) |
62 | 10, 60, 61 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (πΉβπ) β (BaseβπΊ)) |
63 | 62 | snssd 4773 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β {(πΉβπ)} β (BaseβπΊ)) |
64 | 9, 50 | cntzsubm 19124 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ {(πΉβπ)} β (BaseβπΊ)) β ((CntzβπΊ)β{(πΉβπ)}) β (SubMndβπΊ)) |
65 | 56, 63, 64 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β ((CntzβπΊ)β{(πΉβπ)}) β (SubMndβπΊ)) |
66 | 12 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β π»:πΌβΆ(BaseβπΊ)) |
67 | 66 | ffnd 6673 |
. . . . . . . . 9
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β π» Fn πΌ) |
68 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β π₯ β πΌ) |
69 | | fnssres 6628 |
. . . . . . . . 9
β’ ((π» Fn πΌ β§ π₯ β πΌ) β (π» βΎ π₯) Fn π₯) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (π» βΎ π₯) Fn π₯) |
71 | | fvres 6865 |
. . . . . . . . . . 11
β’ (π¦ β π₯ β ((π» βΎ π₯)βπ¦) = (π»βπ¦)) |
72 | 71 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β ((π» βΎ π₯)βπ¦) = (π»βπ¦)) |
73 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β πΊdom DProd π) |
74 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β dom π = πΌ) |
75 | 73, 74 | dprdf2 19794 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π:πΌβΆ(SubGrpβπΊ)) |
76 | 60 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π β πΌ) |
77 | 75, 76 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (πβπ) β (SubGrpβπΊ)) |
78 | 9 | subgss 18937 |
. . . . . . . . . . . . 13
β’ ((πβπ) β (SubGrpβπΊ) β (πβπ) β (BaseβπΊ)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (πβπ) β (BaseβπΊ)) |
80 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β πΉ β π) |
81 | 4, 73, 74, 80 | dprdfcl 19800 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β§ π β πΌ) β (πΉβπ) β (πβπ)) |
82 | 76, 81 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (πΉβπ) β (πβπ)) |
83 | 82 | snssd 4773 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β {(πΉβπ)} β (πβπ)) |
84 | 9, 50 | cntz2ss 19121 |
. . . . . . . . . . . 12
β’ (((πβπ) β (BaseβπΊ) β§ {(πΉβπ)} β (πβπ)) β ((CntzβπΊ)β(πβπ)) β ((CntzβπΊ)β{(πΉβπ)})) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β ((CntzβπΊ)β(πβπ)) β ((CntzβπΊ)β{(πΉβπ)})) |
86 | 68 | sselda 3948 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π¦ β πΌ) |
87 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π¦ β π₯) |
88 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π β (πΌ β π₯)) |
89 | 88 | eldifbd 3927 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β Β¬ π β π₯) |
90 | | nelne2 3039 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π₯ β§ Β¬ π β π₯) β π¦ β π) |
91 | 87, 89, 90 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π¦ β π) |
92 | 73, 74, 86, 76, 91, 50 | dprdcntz 19795 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (πβπ¦) β ((CntzβπΊ)β(πβπ))) |
93 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β π» β π) |
94 | 4, 73, 74, 93 | dprdfcl 19800 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β§ π¦ β πΌ) β (π»βπ¦) β (πβπ¦)) |
95 | 86, 94 | mpdan 686 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (π»βπ¦) β (πβπ¦)) |
96 | 92, 95 | sseldd 3949 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (π»βπ¦) β ((CntzβπΊ)β(πβπ))) |
97 | 85, 96 | sseldd 3949 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β (π»βπ¦) β ((CntzβπΊ)β{(πΉβπ)})) |
98 | 72, 97 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β§ π¦ β π₯) β ((π» βΎ π₯)βπ¦) β ((CntzβπΊ)β{(πΉβπ)})) |
99 | 98 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β βπ¦ β π₯ ((π» βΎ π₯)βπ¦) β ((CntzβπΊ)β{(πΉβπ)})) |
100 | | ffnfv 7070 |
. . . . . . . 8
β’ ((π» βΎ π₯):π₯βΆ((CntzβπΊ)β{(πΉβπ)}) β ((π» βΎ π₯) Fn π₯ β§ βπ¦ β π₯ ((π» βΎ π₯)βπ¦) β ((CntzβπΊ)β{(πΉβπ)}))) |
101 | 70, 99, 100 | sylanbrc 584 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (π» βΎ π₯):π₯βΆ((CntzβπΊ)β{(πΉβπ)})) |
102 | | resss 5966 |
. . . . . . . . . 10
β’ (π» βΎ π₯) β π» |
103 | 102 | rnssi 5899 |
. . . . . . . . 9
β’ ran
(π» βΎ π₯) β ran π» |
104 | 50 | cntzidss 19126 |
. . . . . . . . 9
β’ ((ran
π» β
((CntzβπΊ)βran
π») β§ ran (π» βΎ π₯) β ran π») β ran (π» βΎ π₯) β ((CntzβπΊ)βran (π» βΎ π₯))) |
105 | 54, 103, 104 | sylancl 587 |
. . . . . . . 8
β’ (π β ran (π» βΎ π₯) β ((CntzβπΊ)βran (π» βΎ π₯))) |
106 | 105 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β ran (π» βΎ π₯) β ((CntzβπΊ)βran (π» βΎ π₯))) |
107 | 21, 27 | fsuppres 9338 |
. . . . . . . 8
β’ (π β (π» βΎ π₯) finSupp 0 ) |
108 | 107 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (π» βΎ π₯) finSupp 0 ) |
109 | 25, 50, 56, 58, 65, 101, 106, 108 | gsumzsubmcl 19703 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (πΊ Ξ£g (π» βΎ π₯)) β ((CntzβπΊ)β{(πΉβπ)})) |
110 | 109 | snssd 4773 |
. . . . 5
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β {(πΊ Ξ£g (π» βΎ π₯))} β ((CntzβπΊ)β{(πΉβπ)})) |
111 | 66, 68 | fssresd 6713 |
. . . . . . . 8
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (π» βΎ π₯):π₯βΆ(BaseβπΊ)) |
112 | 9, 25, 50, 56, 58, 111, 106, 108 | gsumzcl 19696 |
. . . . . . 7
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (πΊ Ξ£g (π» βΎ π₯)) β (BaseβπΊ)) |
113 | 112 | snssd 4773 |
. . . . . 6
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β {(πΊ Ξ£g (π» βΎ π₯))} β (BaseβπΊ)) |
114 | 9, 50 | cntzrec 19122 |
. . . . . 6
β’ (({(πΊ Ξ£g
(π» βΎ π₯))} β (BaseβπΊ) β§ {(πΉβπ)} β (BaseβπΊ)) β ({(πΊ Ξ£g (π» βΎ π₯))} β ((CntzβπΊ)β{(πΉβπ)}) β {(πΉβπ)} β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))}))) |
115 | 113, 63, 114 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β ({(πΊ Ξ£g (π» βΎ π₯))} β ((CntzβπΊ)β{(πΉβπ)}) β {(πΉβπ)} β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))}))) |
116 | 110, 115 | mpbid 231 |
. . . 4
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β {(πΉβπ)} β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))})) |
117 | | fvex 6859 |
. . . . 5
β’ (πΉβπ) β V |
118 | 117 | snss 4750 |
. . . 4
β’ ((πΉβπ) β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))}) β {(πΉβπ)} β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))})) |
119 | 116, 118 | sylibr 233 |
. . 3
β’ ((π β§ (π₯ β πΌ β§ π β (πΌ β π₯))) β (πΉβπ) β ((CntzβπΊ)β{(πΊ Ξ£g (π» βΎ π₯))})) |
120 | 9, 25, 17, 50, 51, 3, 20, 21, 52, 10, 12, 53, 54, 55, 119 | gsumzaddlem 19706 |
. 2
β’ (π β (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»))) |
121 | 49, 120 | jca 513 |
1
β’ (π β ((πΉ βf + π») β π β§ (πΊ Ξ£g (πΉ βf + π»)) = ((πΊ Ξ£g πΉ) + (πΊ Ξ£g π»)))) |