This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )