Theorem cnfldmulg

Description: The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Assertion	cnfldmulg	$$⊢\left(A\in \mathbb{Z}\wedge B\in ℂ\right)\to A{\cdot }_{{ℂ}_{\mathrm{fld}}}B=AB$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=0\to x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=0{\cdot }_{{ℂ}_{\mathrm{fld}}}B$$
2		oveq1	$$⊢x=0\to xB=0\cdot B$$
3	1 2	eqeq12d	$$⊢x=0\to \left(x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=xB\leftrightarrow 0{\cdot }_{{ℂ}_{\mathrm{fld}}}B=0\cdot B\right)$$
4		oveq1	$$⊢x=y\to x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=y{\cdot }_{{ℂ}_{\mathrm{fld}}}B$$
5		oveq1	$$⊢x=y\to xB=yB$$
6	4 5	eqeq12d	$$⊢x=y\to \left(x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=xB\leftrightarrow y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\right)$$
7		oveq1	$$⊢x=y+1\to x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B$$
8		oveq1	$$⊢x=y+1\to xB=\left(y+1\right)B$$
9	7 8	eqeq12d	$$⊢x=y+1\to \left(x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=xB\leftrightarrow \left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y+1\right)B\right)$$
10		oveq1	$$⊢x=-y\to x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B$$
11		oveq1	$$⊢x=-y\to xB=\left(-y\right)B$$
12	10 11	eqeq12d	$$⊢x=-y\to \left(x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=xB\leftrightarrow \left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(-y\right)B\right)$$
13		oveq1	$$⊢x=A\to x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=A{\cdot }_{{ℂ}_{\mathrm{fld}}}B$$
14		oveq1	$$⊢x=A\to xB=AB$$
15	13 14	eqeq12d	$$⊢x=A\to \left(x{\cdot }_{{ℂ}_{\mathrm{fld}}}B=xB\leftrightarrow A{\cdot }_{{ℂ}_{\mathrm{fld}}}B=AB\right)$$
16		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
17		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
18		eqid	$$⊢{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
19	16 17 18	mulg0	$$⊢B\in ℂ\to 0{\cdot }_{{ℂ}_{\mathrm{fld}}}B=0$$
20		mul02	$$⊢B\in ℂ\to 0\cdot B=0$$
21	19 20	eqtr4d	$$⊢B\in ℂ\to 0{\cdot }_{{ℂ}_{\mathrm{fld}}}B=0\cdot B$$
22		oveq1	$$⊢y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)+B=yB+B$$
23		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
24		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
25	23 24	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
26		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
27	16 18 26	mulgnn0p1	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to \left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)+B$$
28	25 27	mp3an1	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to \left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)+B$$
29		nn0cn	$$⊢y\in {\mathbb{N}}_0\to y\in ℂ$$
30	29	adantr	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to y\in ℂ$$
31		simpr	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to B\in ℂ$$
32	30 31	adddirp1d	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to \left(y+1\right)B=yB+B$$
33	28 32	eqeq12d	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to \left(\left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y+1\right)B\leftrightarrow \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)+B=yB+B\right)$$
34	22 33	imbitrrid	$$⊢\left(y\in {\mathbb{N}}_0\wedge B\in ℂ\right)\to \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to \left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y+1\right)B\right)$$
35	34	expcom	$$⊢B\in ℂ\to \left(y\in {\mathbb{N}}_0\to \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to \left(y+1\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(y+1\right)B\right)\right)$$
36		fveq2	$$⊢y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(yB\right)$$
37		eqid	$$⊢{inv}_g\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)$$
38	16 18 37	mulgnegnn	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to \left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B={inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)$$
39		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
40		mulneg1	$$⊢\left(y\in ℂ\wedge B\in ℂ\right)\to \left(-y\right)B=-yB$$
41	39 40	sylan	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to \left(-y\right)B=-yB$$
42		mulcl	$$⊢\left(y\in ℂ\wedge B\in ℂ\right)\to yB\in ℂ$$
43	39 42	sylan	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to yB\in ℂ$$
44		cnfldneg	$$⊢yB\in ℂ\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(yB\right)=-yB$$
45	43 44	syl	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(yB\right)=-yB$$
46	41 45	eqtr4d	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to \left(-y\right)B={inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(yB\right)$$
47	38 46	eqeq12d	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to \left(\left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(-y\right)B\leftrightarrow {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(yB\right)\right)$$
48	36 47	imbitrrid	$$⊢\left(y\in \mathbb{N}\wedge B\in ℂ\right)\to \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to \left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(-y\right)B\right)$$
49	48	expcom	$$⊢B\in ℂ\to \left(y\in \mathbb{N}\to \left(y{\cdot }_{{ℂ}_{\mathrm{fld}}}B=yB\to \left(-y\right){\cdot }_{{ℂ}_{\mathrm{fld}}}B=\left(-y\right)B\right)\right)$$
50	3 6 9 12 15 21 35 49	zindd	$$⊢B\in ℂ\to \left(A\in \mathbb{Z}\to A{\cdot }_{{ℂ}_{\mathrm{fld}}}B=AB\right)$$
51	50	impcom	$$⊢\left(A\in \mathbb{Z}\wedge B\in ℂ\right)\to A{\cdot }_{{ℂ}_{\mathrm{fld}}}B=AB$$