mulid - Metamath Proof Explorer

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

Theorem mulid 25758

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 25757	. . . 4 $\$ $\$
2		ablogrpo 25686	. . . 4 $\$ $\$ $\$ $\$
3	1, 2	ax-mp 5	. . 3 $\$ $\$
4		mulnzcnopr 10235	. . . . . 6 $\$ $\$ $\$ $\$ $\$
5	4	fdmi 5718	. . . . 5 $\$ $\$ $\$ $\$
6	3, 5	grporn 25614	. . . 4 $\$ $\$ $\$
7		eqid 2402	. . . 4 GId $\$ $\$ GId $\$ $\$
8	6, 7	grpoidval 25618	. . 3 $\$ $\$ GId $\$ $\$ $\$ $\$ $\$ $\$
9	3, 8	ax-mp 5	. 2 GId $\$ $\$ $\$ $\$ $\$ $\$
10		ax-1cn 9579	. . . . . . 7
11		ax-1ne0 9590	. . . . . . 7
12		eldifsn 4096	. . . . . . 7 $\$ $/\$
13	10, 11, 12	mpbir2an 921	. . . . . 6 $\$
14		ovres 6422	. . . . . 6 $\$ $/\$ $\$ $\$ $\$
15	13, 14	mpan 668	. . . . 5 $\$ $\$ $\$
16		eldifi 3564	. . . . . 6 $\$
17	16	mulid2d 9643	. . . . 5 $\$
18	15, 17	eqtrd 2443	. . . 4 $\$ $\$ $\$
19	18	rgen 2763	. . 3 $\$ $\$ $\$
20	6	grpoideu 25611	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
21	3, 20	ax-mp 5	. . . 4 $\$ $\$ $\$ $\$
22		oveq1 6284	. . . . . . 7 $\$ $\$ $\$ $\$
23	22	eqeq1d 2404	. . . . . 6 $\$ $\$ $\$ $\$
24	23	ralbidv 2842	. . . . 5 $\$ $\$ $\$ $\$ $\$ $\$
25	24	riota2 6261	. . . 4 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
26	13, 21, 25	mp2an 670	. . 3 $\$ $\$ $\$ $\$ $\$ $\$ $\$
27	19, 26	mpbi 208	. 2 $\$ $\$ $\$ $\$
28	9, 27	eqtri 2431	1 GId $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wb 184

wceq 1405

wcel 1842

wne 2598

wral 2753

wreu 2755 $\$ cdif 3410

csn 3971

cxp 4820

cres 4824

cfv 5568

crio 6238 (class class class)co 6277

cc 9519

cc0 9521

c1 9522

cmul 9526

cgr 25588 GIdcgi 25589

cablo 25683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598 ax-mulf 9601

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-op 3978 df-uni 4191 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-id 4737 df-po 4743 df-so 4744 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-er 7347 df-en 7554 df-dom 7555 df-sdom 7556 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-div 10247 df-grpo 25593 df-gid 25594 df-ablo 25684

This theorem is referenced by: (None)

W3C validator