Theorem mulrid 8324

Description: 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
mulrid	|- ( A e. CC -> ( A x. 1 ) = A )

Proof of Theorem mulrid

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnre 8323	. 2 |- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
2		recn 8313	. . . . . 6 |- ( x e. RR -> x e. CC )
3		ax-icn 8275	. . . . . . 7 |- _i e. CC
4		recn 8313	. . . . . . 7 |- ( y e. RR -> y e. CC )
5		mulcl 8307	. . . . . . 7 |- ( ( _i e. CC /\ y e. CC ) -> ( _i x. y ) e. CC )
6	3, 4, 5	sylancr 418	. . . . . 6 |- ( y e. RR -> ( _i x. y ) e. CC )
7		ax-1cn 8273	. . . . . . 7 |- 1 e. CC
8		adddir 8318	. . . . . . 7 |- ( ( x e. CC /\ ( _i x. y ) e. CC /\ 1 e. CC ) -> ( ( x + ( _i x. y ) ) x. 1 ) = ( ( x x. 1 ) + ( ( _i x. y ) x. 1 ) ) )
9	7, 8	mp3an3 1367	. . . . . 6 |- ( ( x e. CC /\ ( _i x. y ) e. CC ) -> ( ( x + ( _i x. y ) ) x. 1 ) = ( ( x x. 1 ) + ( ( _i x. y ) x. 1 ) ) )
10	2, 6, 9	syl2an 289	. . . . 5 |- ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) x. 1 ) = ( ( x x. 1 ) + ( ( _i x. y ) x. 1 ) ) )
11		ax-1rid 8287	. . . . . 6 |- ( x e. RR -> ( x x. 1 ) = x )
12		mulass 8311	. . . . . . . . 9 |- ( ( _i e. CC /\ y e. CC /\ 1 e. CC ) -> ( ( _i x. y ) x. 1 ) = ( _i x. ( y x. 1 ) ) )
13	3, 7, 12	mp3an13 1369	. . . . . . . 8 |- ( y e. CC -> ( ( _i x. y ) x. 1 ) = ( _i x. ( y x. 1 ) ) )
14	4, 13	syl 14	. . . . . . 7 |- ( y e. RR -> ( ( _i x. y ) x. 1 ) = ( _i x. ( y x. 1 ) ) )
15		ax-1rid 8287	. . . . . . . 8 |- ( y e. RR -> ( y x. 1 ) = y )
16	15	oveq2d 6101	. . . . . . 7 |- ( y e. RR -> ( _i x. ( y x. 1 ) ) = ( _i x. y ) )
17	14, 16	eqtrd 2271	. . . . . 6 |- ( y e. RR -> ( ( _i x. y ) x. 1 ) = ( _i x. y ) )
18	11, 17	oveqan12d 6104	. . . . 5 |- ( ( x e. RR /\ y e. RR ) -> ( ( x x. 1 ) + ( ( _i x. y ) x. 1 ) ) = ( x + ( _i x. y ) ) )
19	10, 18	eqtrd 2271	. . . 4 |- ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) x. 1 ) = ( x + ( _i x. y ) ) )
20		oveq1 6092	. . . . 5 |- ( A = ( x + ( _i x. y ) ) -> ( A x. 1 ) = ( ( x + ( _i x. y ) ) x. 1 ) )
21		id 19	. . . . 5 |- ( A = ( x + ( _i x. y ) ) -> A = ( x + ( _i x. y ) ) )
22	20, 21	eqeq12d 2253	. . . 4 |- ( A = ( x + ( _i x. y ) ) -> ( ( A x. 1 ) = A <-> ( ( x + ( _i x. y ) ) x. 1 ) = ( x + ( _i x. y ) ) ) )
23	19, 22	syl5ibrcom 157	. . 3 |- ( ( x e. RR /\ y e. RR ) -> ( A = ( x + ( _i x. y ) ) -> ( A x. 1 ) = A ) )
24	23	rexlimivv 2674	. 2 |- ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> ( A x. 1 ) = A )
25	1, 24	syl 14	1 |- ( A e. CC -> ( A x. 1 ) = A )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   E.wrex 2529  (class class class)co 6085   CCcc 8178   RRcr 8179   1c1 8181   _ici 8182   + caddc 8183   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8272  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-mulcom 8281  ax-mulass 8283  ax-distr 8284  ax-1rid 8287  ax-cnre 8291

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  mullid  8325  mulridi  8329  mulridd  8344  muleqadd  9001  divdivap1  9056  conjmulap  9062  nnmulcl  9328  expmul  11036  binom21  11104  binom2sub1  11106  bernneq  11113  hashiun  12264  fproddccvg  12358  prodmodclem2a  12362  efexp  12468  cncrng  14990  cnfld1  14993  ecxp  16098  lgsdilem2  16321