Theorem mulid 8069

Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.)

Assertion

Ref	Expression
mulid	|- (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1

Proof of Theorem mulid

Step	Hyp	Ref	Expression
1		eldifsn 2453	. . . . . 6 |- (1 e. (CC \ {0}) <-> (1 e. CC /\ 1 =/= 0))
2		ax1cn 5241	. . . . . 6 |- 1 e. CC
3		ax1ne0 5252	. . . . . 6 |- 1 =/= 0
4	1, 2, 3	mpbir2an 728	. . . . 5 |- 1 e. (CC \ {0})
5		oprvalres 4018	. . . . 5 |- ((1 e. (CC \ {0}) /\ x e. (CC \ {0})) -> (1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = (1 x. x))
6	4, 5	mpan 693	. . . 4 |- (x e. (CC \ {0}) -> (1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = (1 x. x))
7		eldifi 2152	. . . . 5 |- (x e. (CC \ {0}) -> x e. CC)
8		mulid2t 5389	. . . . 5 |- (x e. CC -> (1 x. x) = x)
9	7, 8	syl 10	. . . 4 |- (x e. (CC \ {0}) -> (1 x. x) = x)
10	6, 9	eqtrd 1499	. . 3 |- (x e. (CC \ {0}) -> (1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x)
11	10	rgen 1690	. 2 |- A.x e. (CC \ {0})(1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x
12		opreq1 3953	. . . . . . 7 |- (y = 1 -> (y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = (1( x. |` ((CC \ {0}) X. (CC \ {0})))x))
13	12	eqeq1d 1475	. . . . . 6 |- (y = 1 -> ((y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> (1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x))
14	13	ralbidv 1655	. . . . 5 |- (y = 1 -> (A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> A.x e. (CC \ {0})(1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x))
15		ablmul 8068	. . . . . . . 8 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Abel
16		ablgrp 8038	. . . . . . . 8 |- (( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Abel -> ( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Grp)
17	15, 16	ax-mp 7	. . . . . . 7 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Grp
18		mulnzcnopr 5671	. . . . . . . . 9 |- ( x. |` ((CC \ {0}) X. (CC \ {0}))):((CC \ {0}) X. (CC \ {0}))-->(CC \ {0})
19	17, 18	grprnOLD 7991	. . . . . . . 8 |- (CC \ {0}) = ran ( x. |` ((CC \ {0}) X. (CC \ {0})))
20		eqid 1468	. . . . . . . 8 |- (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = (Id` ( x. |` ((CC \ {0}) X. (CC \ {0}))))
21	19, 20	grpidval 7992	. . . . . . 7 |- (( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Grp -> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x})
22	17, 21	ax-mp 7	. . . . . 6 |- (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x}
23		eqeq12 1479	. . . . . . 7 |- ((U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) /\ y = 1) -> (U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y <-> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1))
24		eqcom 1469	. . . . . . 7 |- ((Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} <-> U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))))
25	23, 24	sylanb 449	. . . . . 6 |- (((Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} /\ y = 1) -> (U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y <-> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1))
26	22, 25	mpan 693	. . . . 5 |- (y = 1 -> (U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y <-> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1))
27	14, 26	bibi12d 627	. . . 4 |- (y = 1 -> ((A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y) <-> (A.x e. (CC \ {0})(1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1)))
28	19	grpideu 7987	. . . . . 6 |- (( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Grp -> E!y e. (CC \ {0})A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x)
29	17, 28	ax-mp 7	. . . . 5 |- E!y e. (CC \ {0})A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x
30		reuuni1 2872	. . . . 5 |- ((y e. (CC \ {0}) /\ E!y e. (CC \ {0})A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x) -> (A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y))
31	29, 30	mpan2 694	. . . 4 |- (y e. (CC \ {0}) -> (A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> U.{y e. (CC \ {0}) | A.x e. (CC \ {0})(y( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x} = y))
32	27, 31	vtoclga 1843	. . 3 |- (1 e. (CC \ {0}) -> (A.x e. (CC \ {0})(1( x. |` ((CC \ {0}) X. (CC \ {0})))x) = x <-> (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1))
33	4, 32	ax-mp 7	. 2 |- (A.x e. (CC \ {0})(1( x. |` (