Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Definition df-cj 6684

Description: Define the complex conjugate function. See cjcl 6699 for its closure and cjvalt 6695 for its value.

Assertion

Ref	Expression
df-cj

Distinct variable group:   ,

---

Detailed syntax breakdown of Definition df-cj

Step	Hyp	Ref	Expression
1		ccj 6680	. 2
2		vx	. . . . . 6
3	2	cv 952	. . . . 5
4		cc 5204	. . . . 5
5	3, 4	wcel 955	. . . 4
6		vy	. . . . . 6
7	6	cv 952	. . . . 5
8		cre 6678	. . . . . . 7
9	3, 8	cfv 3172	. . . . . 6
10		ci 5208	. . . . . . 7
11		cim 6679	. . . . . . . 8
12	3, 11	cfv 3172	. . . . . . 7
13		cmul 5211	. . . . . . 7
14	10, 12, 13	co 3948	. . . . . 6
15		cmin 5264	. . . . . 6
16	9, 14, 15	co 3948	. . . . 5
17	7, 16	wceq 953	. . . 4
18	5, 17	wa 223	. . 3
19	18, 2, 6	copab 2656	. 2
20	1, 19	wceq 953	1

Colors of variables: wff set class

This definition is referenced by:  cjvalt 6695  cjcncf 7213

Copyright terms: Public domain