Description: The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015) (Revisd by AV, 28-Jan-2020.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mgmplusf.1 | ||
mgmplusf.2 | |||
Assertion | mgmplusf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgmplusf.1 | ||
2 | mgmplusf.2 | ||
3 | eqid | ||
4 | 1 3 | mgmcl | |
5 | 4 | 3expb | |
6 | 5 | ralrimivva | |
7 | 1 3 2 | plusffval | |
8 | 7 | fmpo | |
9 | 6 8 | sylib |