Theorem cjmul 4819

Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133.

Hypotheses

Ref	Expression
cjcj.1	|- A e. CC
readd.2	|- B e. CC

Assertion

Ref	Expression
cjmul	|- (*` (A x. B)) = ((*` A) x. (*` B))

Proof of Theorem cjmul

Step	Hyp	Ref	Expression
1		cjcj.1	. . . . . . . . 9 |- A e. CC
2	1	recl 4802	. . . . . . . 8 |- (Re` A) e. RR
3		readd.2	. . . . . . . . 9 |- B e. CC
4	3	recl 4802	. . . . . . . 8 |- (Re` B) e. RR
5	2, 4	remulcl 4119	. . . . . . 7 |- ((Re` A) x. (Re` B)) e. RR
6	1	imcl 4803	. . . . . . . 8 |- (Im` A) e. RR
7	3	imcl 4803	. . . . . . . 8 |- (Im` B) e. RR
8	6, 7	remulcl 4119	. . . . . . 7 |- ((Im` A) x. (Im` B)) e. RR
9	5, 8	resubcl 4174	. . . . . 6 |- (((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) e. RR
10	9	recn 4098	. . . . 5 |- (((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) e. CC
11	2, 7	remulcl 4119	. . . . . . . 8 |- ((Re` A) x. (Im` B)) e. RR
12	6, 4	remulcl 4119	. . . . . . . 8 |- ((Im` A) x. (Re` B)) e. RR
13	11, 12	readdcl 4118	. . . . . . 7 |- (((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) e. RR
14	13	recn 4098	. . . . . 6 |- (((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) e. CC
15		axicn 4065	. . . . . 6 |- i e. CC
16	14, 15	mulcl 4105	. . . . 5 |- ((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i) e. CC
17	10, 16	subneg 4148	. . . 4 |- ((((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) - ((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i)) = ((((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) + -u((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i))
18	6	recn 4098	. . . . . . . 8 |- (Im` A) e. CC
19	7	recn 4098	. . . . . . . 8 |- (Im` B) e. CC
20	18, 19	mul2neg 4192	. . . . . . 7 |- (-u(Im` A) x. -u(Im` B)) = ((Im` A) x. (Im` B))
21	20	cleqcomi 1105	. . . . . 6 |- ((Im` A) x. (Im` B)) = (-u(Im` A) x. -u(Im` B))
22	21	opreq2i 3010	. . . . 5 |- (((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) = (((Re` A) x. (Re` B)) - (-u(Im` A) x. -u(Im` B)))
23	14, 15	mulneg1 4190	. . . . . 6 |- (-u(((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i) = -u((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i)
24	11	recn 4098	. . . . . . . . 9 |- ((Re` A) x. (Im` B)) e. CC
25	12	recn 4098	. . . . . . . . 9 |- ((Im` A) x. (Re` B)) e. CC
26	24, 25	negdi 4193	. . . . . . . 8 |- -u(((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) = (-u((Re` A) x. (Im` B)) + -u((Im` A) x. (Re` B)))
27	2	recn 4098	. . . . . . . . . 10 |- (Re` A) e. CC
28	27, 19	mulneg2 4191	. . . . . . . . 9 |- ((Re` A) x. -u(Im` B)) = -u((Re` A) x. (Im` B))
29	4	recn 4098	. . . . . . . . . 10 |- (Re` B) e. CC
30	18, 29	mulneg1 4190	. . . . . . . . 9 |- (-u(Im` A) x. (Re` B)) = -u((Im` A) x. (Re` B))
31	28, 30	opreq12i 3011	. . . . . . . 8 |- (((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) = (-u((Re` A) x. (Im` B)) + -u((Im` A) x. (Re` B)))
32	26, 31	eqtr4 1122	. . . . . . 7 |- -u(((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) = (((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B)))
33	32	opreq1i 3009	. . . . . 6 |- (-u(((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i) = ((((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) x. i)
34	23, 33	eqtr3 1121	. . . . 5 |- -u((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i) = ((((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) x. i)
35	22, 34	opreq12i 3011	. . . 4 |- ((((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) + -u((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i)) = ((((Re` A) x. (Re` B)) - (-u(Im` A) x. -u(Im` B))) + ((((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) x. i))
36	17, 35	eqtr 1119	. . 3 |- ((((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) - ((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i)) = ((((Re` A) x. (Re` B)) - (-u(Im` A) x. -u(Im` B))) + ((((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) x. i))
37	1, 3	remul 4816	. . . 4 |- (Re` (A x. B)) = (((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B)))
38	1, 3	immul 4817	. . . . 5 |- (Im` (A x. B)) = (((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B)))
39	38	opreq1i 3009	. . . 4 |- ((Im` (A x. B)) x. i) = ((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i)
40	37, 39	opreq12i 3011	. . 3 |- ((Re` (A x. B)) - ((Im` (A x. B)) x. i)) = ((((Re` A) x. (Re` B)) - ((Im` A) x. (Im` B))) - ((((Re` A) x. (Im` B)) + ((Im` A) x. (Re` B))) x. i))
41	6	renegcl 4171	. . . 4 |- -u(Im` A) e. RR
42	7	renegcl 4171	. . . 4 |- -u(Im` B) e. RR
43	2, 41, 4, 42	crmult 4530	. . 3 |- (((Re` A) + (-u(Im` A) x. i)) x. ((Re` B) + (-u(Im` B) x. i))) = ((((Re` A) x. (Re` B)) - (-u(Im` A) x. -u(Im` B))) + ((((Re` A) x. -u(Im` B)) + (-u(Im` A) x. (Re` B))) x. i))
44	36, 40, 43	3eqtr4 1126	. 2 |- ((Re` (A x. B)) - ((Im` (A x. B)) x. i)) = (((Re` A) + (-u(Im` A) x. i)) x. ((Re` B) + (-u(Im` B) x. i)))
45	1, 3	mulcl 4105	. . 3 |- (A x. B) e. CC
46		cjvalt 4799	. . 3 |- ((A x. B) e. CC -> (*` (A x. B)) = ((Re` (A x. B)) - ((Im` (A x. B)) x. i)))
47	45, 46	ax-mp 6	. 2 |- (*` (A x. B)) = ((Re` (A x. B)) - ((Im` (A x. B)) x. i))
48	18, 15	mulcl 4105	. . . . 5 |- ((Im` A) x. i) e. CC
49	27, 48	subneg 4148	. . . 4 |- ((Re` A) - ((Im` A) x. i)) = ((Re` A) + -u((Im` A) x. i))
50		cjvalt 4799	. . . . 5 |- (A e. CC -> (*` A) = ((Re` A) - ((Im` A) x. i)))
51	1, 50	ax-mp 6	. . . 4 |- (*` A) = ((Re` A) - ((Im` A) x. i))
52	18, 15	mulneg1 4190	. . . . 5 |- (-u(Im` A) x. i) = -u((Im` A) x. i)
53	52	opreq2i 3010	. . . 4 |- ((Re` A) + (-u(Im` A) x. i)) = ((Re` A) + -u((Im` A) x. i))
54	49, 51, 53	3eqtr4 1126	. . 3 |- (*` A) = ((Re` A) + (-u(Im` A) x. i))
55	19, 15	mulcl 4105	. . . . 5 |- ((Im` B) x. i) e. CC
56	29, 55	subneg 4148	. . . 4 |- ((Re` B) - ((Im` B) x. i)) = ((Re` B) + -u((Im` B) x. i))
57		cjvalt 4799<