Theorem cnidOLD

Description: Obsolete version of cnaddid . The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	cnidOLD	⊢ 0 = ( GId ‘ + )

Proof

Step	Hyp	Ref	Expression
1		cnaddabloOLD	⊢ + ∈ AbelOp
2		ablogrpo	⊢ ( + ∈ AbelOp → + ∈ GrpOp )
3	1 2	ax-mp	⊢ + ∈ GrpOp
4		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
5	4	fdmi	⊢ dom + = ( ℂ × ℂ )
6	3 5	grporn	⊢ ℂ = ran +
7		eqid	⊢ ( GId ‘ + ) = ( GId ‘ + )
8	6 7	grpoidval	⊢ ( + ∈ GrpOp → ( GId ‘ + ) = ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) )
9	3 8	ax-mp	⊢ ( GId ‘ + ) = ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 )
10		addlid	⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
11	10	rgen	⊢ ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥
12		0cn	⊢ 0 ∈ ℂ
13	6	grpoideu	⊢ ( + ∈ GrpOp → ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 )
14	3 13	ax-mp	⊢ ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥
15		oveq1	⊢ ( 𝑦 = 0 → ( 𝑦 + 𝑥 ) = ( 0 + 𝑥 ) )
16	15	eqeq1d	⊢ ( 𝑦 = 0 → ( ( 𝑦 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
17	16	ralbidv	⊢ ( 𝑦 = 0 → ( ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ) )
18	17	riota2	⊢ ( ( 0 ∈ ℂ ∧ ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) → ( ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0 ) )
19	12 14 18	mp2an	⊢ ( ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0 )
20	11 19	mpbi	⊢ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0
21	9 20	eqtr2i	⊢ 0 = ( GId ‘ + )