mulid - Metamath Proof Explorer

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

Theorem mulid 26084

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 26083	. . . 4 $\$ $\$
2		ablogrpo 26012	. . . 4 $\$ $\$ $\$ $\$
3	1, 2	ax-mp 5	. . 3 $\$ $\$
4		mulnzcnopr 10258	. . . . . 6 $\$ $\$ $\$ $\$ $\$
5	4	fdmi 5734	. . . . 5 $\$ $\$ $\$ $\$
6	3, 5	grporn 25940	. . . 4 $\$ $\$ $\$
7		eqid 2451	. . . 4 GId $\$ $\$ GId $\$ $\$
8	6, 7	grpoidval 25944	. . 3 $\$ $\$ GId $\$ $\$ $\$ $\$ $\$ $\$
9	3, 8	ax-mp 5	. 2 GId $\$ $\$ $\$ $\$ $\$ $\$
10		ax-1cn 9597	. . . . . . 7
11		ax-1ne0 9608	. . . . . . 7
12		eldifsn 4097	. . . . . . 7 $\$ $/\$
13	10, 11, 12	mpbir2an 931	. . . . . 6 $\$
14		ovres 6436	. . . . . 6 $\$ $/\$ $\$ $\$ $\$
15	13, 14	mpan 676	. . . . 5 $\$ $\$ $\$
16		eldifi 3555	. . . . . 6 $\$
17	16	mulid2d 9661	. . . . 5 $\$
18	15, 17	eqtrd 2485	. . . 4 $\$ $\$ $\$
19	18	rgen 2747	. . 3 $\$ $\$ $\$
20	6	grpoideu 25937	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
21	3, 20	ax-mp 5	. . . 4 $\$ $\$ $\$ $\$
22		oveq1 6297	. . . . . . 7 $\$ $\$ $\$ $\$
23	22	eqeq1d 2453	. . . . . 6 $\$ $\$ $\$ $\$
24	23	ralbidv 2827	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
25	24	riota2 6274	. . . 4 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	13, 21, 25	mp2an 678	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$
27	19, 26	mpbi 212	. 2 $\$ $\$ $\$ $\$
28	9, 27	eqtri 2473	1 GId $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wb 188

wceq 1444

wcel 1887

wne 2622

wral 2737

wreu 2739 $\$ cdif 3401

csn 3968

cxp 4832

cres 4836

cfv 5582

crio 6251 (class class class)co 6290

cc 9537

cc0 9539

c1 9540

cmul 9544

cgr 25914 GIdcgi 25915

cablo 26009

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-mulf 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-po 4755 df-so 4756 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-grpo 25919 df-gid 25920 df-ablo 26010

This theorem is referenced by: (None)

W3C validator