Theorem cnfldsub

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

	Ref	Expression
Assertion	cnfldsub	⊢ − = ( -g ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
2		cnfldadd	⊢ + = ( +g ‘ ℂfld )
3		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
4		eqid	⊢ ( -g ‘ ℂfld ) = ( -g ‘ ℂfld )
5	1 2 3 4	grpsubval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( -g ‘ ℂfld ) 𝑦 ) = ( 𝑥 + ( ( invg ‘ ℂfld ) ‘ 𝑦 ) ) )
6		cnfldneg	⊢ ( 𝑦 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑦 ) = - 𝑦 )
7	6	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( invg ‘ ℂfld ) ‘ 𝑦 ) = - 𝑦 )
8	7	oveq2d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + ( ( invg ‘ ℂfld ) ‘ 𝑦 ) ) = ( 𝑥 + - 𝑦 ) )
9		negsub	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + - 𝑦 ) = ( 𝑥 − 𝑦 ) )
10	5 8 9	3eqtrrd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) = ( 𝑥 ( -g ‘ ℂfld ) 𝑦 ) )
11	10	mpoeq3ia	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 ( -g ‘ ℂfld ) 𝑦 ) )
12		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
13		ffn	⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → − Fn ( ℂ × ℂ ) )
14	12 13	ax-mp	⊢ − Fn ( ℂ × ℂ )
15		fnov	⊢ ( − Fn ( ℂ × ℂ ) ↔ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) ) )
16	14 15	mpbi	⊢ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) )
17		cnring	⊢ ℂfld ∈ Ring
18		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
19	17 18	ax-mp	⊢ ℂfld ∈ Grp
20	1 4	grpsubf	⊢ ( ℂfld ∈ Grp → ( -g ‘ ℂfld ) : ( ℂ × ℂ ) ⟶ ℂ )
21		ffn	⊢ ( ( -g ‘ ℂfld ) : ( ℂ × ℂ ) ⟶ ℂ → ( -g ‘ ℂfld ) Fn ( ℂ × ℂ ) )
22	19 20 21	mp2b	⊢ ( -g ‘ ℂfld ) Fn ( ℂ × ℂ )
23		fnov	⊢ ( ( -g ‘ ℂfld ) Fn ( ℂ × ℂ ) ↔ ( -g ‘ ℂfld ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 ( -g ‘ ℂfld ) 𝑦 ) ) )
24	22 23	mpbi	⊢ ( -g ‘ ℂfld ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 ( -g ‘ ℂfld ) 𝑦 ) )
25	11 16 24	3eqtr4i	⊢ − = ( -g ‘ ℂfld )