Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mulg Structured version   Unicode version

Definition df-mulg 14820
 Description: Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)
Assertion
Ref Expression
df-mulg .g
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-mulg
StepHypRef Expression
1 cmg 14694 . 2 .g
2 vg . . 3
3 cvv 2958 . . 3
4 vn . . . 4
5 vx . . . 4
6 cz 10287 . . . 4
72cv 1652 . . . . 5
8 cbs 13474 . . . . 5
97, 8cfv 5457 . . . 4
104cv 1652 . . . . . 6
11 cc0 8995 . . . . . 6
1210, 11wceq 1653 . . . . 5
13 c0g 13728 . . . . . 6
147, 13cfv 5457 . . . . 5
15 vs . . . . . 6
16 cplusg 13534 . . . . . . . 8
177, 16cfv 5457 . . . . . . 7
18 cn 10005 . . . . . . . 8
195cv 1652 . . . . . . . . 9
2019csn 3816 . . . . . . . 8
2118, 20cxp 4879 . . . . . . 7
22 c1 8996 . . . . . . 7
2317, 21, 22cseq 11328 . . . . . 6
24 clt 9125 . . . . . . . 8
2511, 10, 24wbr 4215 . . . . . . 7
2615cv 1652 . . . . . . . 8
2710, 26cfv 5457 . . . . . . 7
2810cneg 9297 . . . . . . . . 9
2928, 26cfv 5457 . . . . . . . 8
30 cminusg 14691 . . . . . . . . 9
317, 30cfv 5457 . . . . . . . 8
3229, 31cfv 5457 . . . . . . 7
3325, 27, 32cif 3741 . . . . . 6
3415, 23, 33csb 3253 . . . . 5
3512, 14, 34cif 3741 . . . 4
364, 5, 6, 9, 35cmpt2 6086 . . 3
372, 3, 36cmpt 4269 . 2
381, 37wceq 1653 1 .g
 Colors of variables: wff set class This definition is referenced by:  mulgfval  14896
 Copyright terms: Public domain W3C validator