mulid - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mulid		Structured version Unicode version

Theorem mulid 23858

Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.) (Revised by Mario Carneiro, 17-Dec-2013.) (New usage is discouraged.)

**Assertion**
Ref	Expression
mulid	GId $\$ $\$

Proof of Theorem mulid Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ablomul 23857	. . . 4 $\$ $\$
2		ablogrpo 23786	. . . 4 $\$ $\$ $\$ $\$
3	1, 2	ax-mp 5	. . 3 $\$ $\$
4		mulnzcnopr 9997	. . . . . 6 $\$ $\$ $\$ $\$ $\$
5	4	fdmi 5579	. . . . 5 $\$ $\$ $\$ $\$
6	3, 5	grporn 23714	. . . 4 $\$ $\$ $\$
7		eqid 2443	. . . 4 GId $\$ $\$ GId $\$ $\$
8	6, 7	grpoidval 23718	. . 3 $\$ $\$ GId $\$ $\$ $\$ $\$ $\$ $\$
9	3, 8	ax-mp 5	. 2 GId $\$ $\$ $\$ $\$ $\$ $\$
10		ax-1cn 9355	. . . . . . 7
11		ax-1ne0 9366	. . . . . . 7
12		eldifsn 4015	. . . . . . 7 $\$ $/\$
13	10, 11, 12	mpbir2an 911	. . . . . 6 $\$
14		ovres 6245	. . . . . 6 $\$ $/\$ $\$ $\$ $\$
15	13, 14	mpan 670	. . . . 5 $\$ $\$ $\$
16		eldifi 3493	. . . . . 6 $\$
17	16	mulid2d 9419	. . . . 5 $\$
18	15, 17	eqtrd 2475	. . . 4 $\$ $\$ $\$
19	18	rgen 2796	. . 3 $\$ $\$ $\$
20	6	grpoideu 23711	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
21	3, 20	ax-mp 5	. . . 4 $\$ $\$ $\$ $\$
22		oveq1 6113	. . . . . . 7 $\$ $\$ $\$ $\$
23	22	eqeq1d 2451	. . . . . 6 $\$ $\$ $\$ $\$
24	23	ralbidv 2750	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
25	24	riota2 6090	. . . 4 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	13, 21, 25	mp2an 672	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$
27	19, 26	mpbi 208	. 2 $\$ $\$ $\$ $\$
28	9, 27	eqtri 2463	1 GId $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1369

wcel 1756

wne 2620

wral 2730

wreu 2732 $\$ cdif 3340

csn 3892

cxp 4853

cres 4857

cfv 5433

crio 6066 (class class class)co 6106

cc 9295

cc0 9297

c1 9298

cmul 9302

cgr 23688 GIdcgi 23689

cablo 23783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4418 ax-sep 4428 ax-nul 4436 ax-pow 4485 ax-pr 4546 ax-un 6387 ax-cnex 9353 ax-resscn 9354 ax-1cn 9355 ax-icn 9356 ax-addcl 9357 ax-addrcl 9358 ax-mulcl 9359 ax-mulrcl 9360 ax-mulcom 9361 ax-addass 9362 ax-mulass 9363 ax-distr 9364 ax-i2m1 9365 ax-1ne0 9366 ax-1rid 9367 ax-rnegex 9368 ax-rrecex 9369 ax-cnre 9370 ax-pre-lttri 9371 ax-pre-lttrn 9372 ax-pre-ltadd 9373 ax-pre-mulgt0 9374 ax-mulf 9377

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2735 df-rex 2736 df-reu 2737 df-rmo 2738 df-rab 2739 df-v 2989 df-sbc 3202 df-csb 3304 df-dif 3346 df-un 3348 df-in 3350 df-ss 3357 df-nul 3653 df-if 3807 df-pw 3877 df-sn 3893 df-pr 3895 df-op 3899 df-uni 4107 df-iun 4188 df-br 4308 df-opab 4366 df-mpt 4367 df-id 4651 df-po 4656 df-so 4657 df-xp 4861 df-rel 4862 df-cnv 4863 df-co 4864 df-dm 4865 df-rn 4866 df-res 4867 df-ima 4868 df-iota 5396 df-fun 5435 df-fn 5436 df-f 5437 df-f1 5438 df-fo 5439 df-f1o 5440 df-fv 5441 df-riota 6067 df-ov 6109 df-oprab 6110 df-mpt2 6111 df-er 7116 df-en 7326 df-dom 7327 df-sdom 7328 df-pnf 9435 df-mnf 9436 df-xr 9437 df-ltxr 9438 df-le 9439 df-sub 9612 df-neg 9613 df-div 10009 df-grpo 23693 df-gid 23694 df-ablo 23784

This theorem is referenced by: (None)

W3C validator