mulid - Metamath Proof Explorer

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

Theorem mulid 25034

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 25033	. . . 4 $\$ $\$
2		ablogrpo 24962	. . . 4 $\$ $\$ $\$ $\$
3	1, 2	ax-mp 5	. . 3 $\$ $\$
4		mulnzcnopr 10191	. . . . . 6 $\$ $\$ $\$ $\$ $\$
5	4	fdmi 5734	. . . . 5 $\$ $\$ $\$ $\$
6	3, 5	grporn 24890	. . . 4 $\$ $\$ $\$
7		eqid 2467	. . . 4 GId $\$ $\$ GId $\$ $\$
8	6, 7	grpoidval 24894	. . 3 $\$ $\$ GId $\$ $\$ $\$ $\$ $\$ $\$
9	3, 8	ax-mp 5	. 2 GId $\$ $\$ $\$ $\$ $\$ $\$
10		ax-1cn 9546	. . . . . . 7
11		ax-1ne0 9557	. . . . . . 7
12		eldifsn 4152	. . . . . . 7 $\$ $/\$
13	10, 11, 12	mpbir2an 918	. . . . . 6 $\$
14		ovres 6424	. . . . . 6 $\$ $/\$ $\$ $\$ $\$
15	13, 14	mpan 670	. . . . 5 $\$ $\$ $\$
16		eldifi 3626	. . . . . 6 $\$
17	16	mulid2d 9610	. . . . 5 $\$
18	15, 17	eqtrd 2508	. . . 4 $\$ $\$ $\$
19	18	rgen 2824	. . 3 $\$ $\$ $\$
20	6	grpoideu 24887	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
21	3, 20	ax-mp 5	. . . 4 $\$ $\$ $\$ $\$
22		oveq1 6289	. . . . . . 7 $\$ $\$ $\$ $\$
23	22	eqeq1d 2469	. . . . . 6 $\$ $\$ $\$ $\$
24	23	ralbidv 2903	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
25	24	riota2 6266	. . . 4 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	13, 21, 25	mp2an 672	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$
27	19, 26	mpbi 208	. 2 $\$ $\$ $\$ $\$
28	9, 27	eqtri 2496	1 GId $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1379

wcel 1767

wne 2662

wral 2814

wreu 2816 $\$ cdif 3473

csn 4027

cxp 4997

cres 5001

cfv 5586

crio 6242 (class class class)co 6282

cc 9486

cc0 9488

c1 9489

cmul 9493

cgr 24864 GIdcgi 24865

cablo 24959

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-po 4800 df-so 4801 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-er 7308 df-en 7514 df-dom 7515 df-sdom 7516 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-grpo 24869 df-gid 24870 df-ablo 24960

This theorem is referenced by: (None)

W3C validator