cnfldsub

Description: The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015)

		Ref	Expression
	Assertion	cnfldsub	$⊢ - = -_{ℂ_{fld}}$

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
2		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
3		eqid	$⊢ {inv}_{g} (ℂ_{fld}) = {inv}_{g} (ℂ_{fld})$
4		eqid	$⊢ -_{ℂ_{fld}} = -_{ℂ_{fld}}$
5	1 2 3 4	grpsubval	$⊢ (x \in ℂ \land y \in ℂ) \to x -_{ℂ_{fld}} y = x + {inv}_{g} (ℂ_{fld}) (y)$
6		cnfldneg	$⊢ y \in ℂ \to {inv}_{g} (ℂ_{fld}) (y) = - y$
7	6	adantl	$⊢ (x \in ℂ \land y \in ℂ) \to {inv}_{g} (ℂ_{fld}) (y) = - y$
8	7	oveq2d	$⊢ (x \in ℂ \land y \in ℂ) \to x + {inv}_{g} (ℂ_{fld}) (y) = x + (- y)$
9		negsub	$⊢ (x \in ℂ \land y \in ℂ) \to x + (- y) = x - y$
10	5 8 9	3eqtrrd	$⊢ (x \in ℂ \land y \in ℂ) \to x - y = x -_{ℂ_{fld}} y$
11	10	mpoeq3ia	$⊢ (x \in ℂ, y \in ℂ ⟼ x - y) = (x \in ℂ, y \in ℂ ⟼ x -_{ℂ_{fld}} y)$
12		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
13		ffn	$⊢ - : ℂ \times ℂ ⟶ ℂ \to - Fn (ℂ \times ℂ)$
14	12 13	ax-mp	$⊢ - Fn (ℂ \times ℂ)$
15		fnov	$⊢ - Fn (ℂ \times ℂ) \leftrightarrow - = (x \in ℂ, y \in ℂ ⟼ x - y)$
16	14 15	mpbi	$⊢ - = (x \in ℂ, y \in ℂ ⟼ x - y)$
17		cnring	$⊢ ℂ_{fld} \in Ring$
18		ringgrp	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Grp$
19	17 18	ax-mp	$⊢ ℂ_{fld} \in Grp$
20	1 4	grpsubf	$⊢ ℂ_{fld} \in Grp \to -_{ℂ_{fld}} : ℂ \times ℂ ⟶ ℂ$
21		ffn	$⊢ -_{ℂ_{fld}} : ℂ \times ℂ ⟶ ℂ \to -_{ℂ_{fld}} Fn (ℂ \times ℂ)$
22	19 20 21	mp2b	$⊢ -_{ℂ_{fld}} Fn (ℂ \times ℂ)$
23		fnov	$⊢ -_{ℂ_{fld}} Fn (ℂ \times ℂ) \leftrightarrow -_{ℂ_{fld}} = (x \in ℂ, y \in ℂ ⟼ x -_{ℂ_{fld}} y)$
24	22 23	mpbi	$⊢ -_{ℂ_{fld}} = (x \in ℂ, y \in ℂ ⟼ x -_{ℂ_{fld}} y)$
25	11 16 24	3eqtr4i	$⊢ - = -_{ℂ_{fld}}$

Metamath Proof Explorer

Theorem cnfldsub

Proof