Theorem lnopunilem1 9891

Description: Lemma for lnopuni 9893.

Hypotheses

Ref	Expression
lnopunilem.1	|- T e. LinOp
lnopunilem.2	|- A.x e. H~ (normh` (T` x)) = (normh` x)
lnopunilem.3	|- A e. H~
lnopunilem.4	|- B e. H~
lnopunilem1.5	|- C e. CC

Assertion

Ref	Expression
lnopunilem1	|- (Re` (C x. ((T` A) .ih (T` B)))) = (Re` (C x. (A .ih B)))

Distinct variable group:   x,T

Proof of Theorem lnopunilem1

Step	Hyp	Ref	Expression
1		lnopunilem.3	. . . . . . . . . 10 |- A e. H~
2		lnopunilem.2	. . . . . . . . . . . 12 |- A.x e. H~ (normh` (T` x)) = (normh` x)
3		fveq2 3719	. . . . . . . . . . . . . . 15 |- (x = y -> (T` x) = (T` y))
4	3	fveq2d 3723	. . . . . . . . . . . . . 14 |- (x = y -> (normh` (T` x)) = (normh` (T` y)))
5		fveq2 3719	. . . . . . . . . . . . . 14 |- (x = y -> (normh` x) = (normh` y))
6	4, 5	eqeq12d 1487	. . . . . . . . . . . . 13 |- (x = y -> ((normh` (T` x)) = (normh` x) <-> (normh` (T` y)) = (normh` y)))
7	6	cbvralv 1797	. . . . . . . . . . . 12 |- (A.x e. H~ (normh` (T` x)) = (normh` x) <-> A.y e. H~ (normh` (T` y)) = (normh` y))
8	2, 7	mpbi 189	. . . . . . . . . . 11 |- A.y e. H~ (normh` (T` y)) = (normh` y)
9		lnopunilem.1	. . . . . . . . . . . . . . . . 17 |- T e. LinOp
10	9	lnopf 9850	. . . . . . . . . . . . . . . 16 |- T:H~-->H~
11	10	ffvelrni 3810	. . . . . . . . . . . . . . 15 |- (y e. H~ -> (T` y) e. H~)
12		normsqt 8956	. . . . . . . . . . . . . . 15 |- ((T` y) e. H~ -> ((normh` (T` y))^2) = ((T` y) .ih (T` y)))
13	11, 12	syl 10	. . . . . . . . . . . . . 14 |- (y e. H~ -> ((normh` (T` y))^2) = ((T` y) .ih (T` y)))
14		normsqt 8956	. . . . . . . . . . . . . 14 |- (y e. H~ -> ((normh` y)^2) = (y .ih y))
15	13, 14	eqeq12d 1487	. . . . . . . . . . . . 13 |- (y e. H~ -> (((normh` (T` y))^2) = ((normh` y)^2) <-> ((T` y) .ih (T` y)) = (y .ih y)))
16		opreq1 3963	. . . . . . . . . . . . 13 |- ((normh` (T` y)) = (normh` y) -> ((normh` (T` y))^2) = ((normh` y)^2))
17	15, 16	syl5bi 208	. . . . . . . . . . . 12 |- (y e. H~ -> ((normh` (T` y)) = (normh` y) -> ((T` y) .ih (T` y)) = (y .ih y)))
18	17	r19.20i 1702	. . . . . . . . . . 11 |- (A.y e. H~ (normh` (T` y)) = (normh` y) -> A.y e. H~ ((T` y) .ih (T` y)) = (y .ih y))
19	8, 18	ax-mp 7	. . . . . . . . . 10 |- A.y e. H~ ((T` y) .ih (T` y)) = (y .ih y)
20		fveq2 3719	. . . . . . . . . . . . 13 |- (y = A -> (T` y) = (T` A))
21	20, 20	opreq12d 3973	. . . . . . . . . . . 12 |- (y = A -> ((T` y) .ih (T` y)) = ((T` A) .ih (T` A)))
22		id 59	. . . . . . . . . . . . 13 |- (y = A -> y = A)
23	22, 22	opreq12d 3973	. . . . . . . . . . . 12 |- (y = A -> (y .ih y) = (A .ih A))
24	21, 23	eqeq12d 1487	. . . . . . . . . . 11 |- (y = A -> (((T` y) .ih (T` y)) = (y .ih y) <-> ((T` A) .ih (T` A)) = (A .ih A)))
25	24	rcla4v 1870	. . . . . . . . . 10 |- (A e. H~ -> (A.y e. H~ ((T` y) .ih (T` y)) = (y .ih y) -> ((T` A) .ih (T` A)) = (A .ih A)))
26	1, 19, 25	mp2 43	. . . . . . . . 9 |- ((T` A) .ih (T` A)) = (A .ih A)
27	26	opreq2i 3967	. . . . . . . 8 |- ((*` C) x. ((T` A) .ih (T` A))) = ((*` C) x. (A .ih A))
28	27	opreq2i 3967	. . . . . . 7 |- (C x. ((*` C) x. ((T` A) .ih (T` A)))) = (C x. ((*` C) x. (A .ih A)))
29		lnopunilem.4	. . . . . . . 8 |- B e. H~
30		fveq2 3719	. . . . . . . . . . 11 |- (y = B -> (T` y) = (T` B))
31	30, 30	opreq12d 3973	. . . . . . . . . 10 |- (y = B -> ((T` y) .ih (T` y)) = ((T` B) .ih (T` B)))
32		id 59	. . . . . . . . . . 11 |- (y = B -> y = B)
33	32, 32	opreq12d 3973	. . . . . . . . . 10 |- (y = B -> (y .ih y) = (B .ih B))
34	31, 33	eqeq12d 1487	. . . . . . . . 9 |- (y = B -> (((T` y) .ih (T` y)) = (y .ih y) <-> ((T` B) .ih (T` B)) = (B .ih B)))
35	34	rcla4v 1870	. . . . . . . 8 |- (B e. H~ -> (A.y e. H~ ((T` y) .ih (T` y)) = (y .ih y) -> ((T` B) .ih (T` B)) = (B .ih B)))
36	29, 19, 35	mp2 43	. . . . . . 7 |- ((T` B) .ih (T` B)) = (B .ih B)
37	28, 36	opreq12i 3968	. . . . . 6 |- ((C x. ((*` C) x. ((T` A) .ih (T` A)))) + ((T` B) .ih (T` B))) = ((C x. ((*` C) x. (A .ih A))) + (B .ih B))
38	37	opreq1i 3966	. . . . 5 |- (((C x. ((*` C) x. ((T` A) .ih (T` A)))) + ((T` B) .ih (T` B))) + ((C x. ((T` A) .ih (T` B))) + (*` (C x. ((T` A) .ih (T` B)))))) = (((C x. ((*` C) x. (A .ih A))) + (B .ih B)) + ((C x. ((T` A) .ih (T` B))) + (*` (C x. ((T` A) .ih (T` B))))))
39		lnopunilem1.5	. . . . . . . . . 10 |- C e. CC
40	39, 1	hvmulcl 8839	. . . . . . . . 9 |- (C .h A) e. H~
41	40, 29	hvaddcl 8843	. . . . . . . 8 |- ((C .h A) +h B) e. H~
42		fveq2 3719	. . . . . . . . . . 11 |- (y = ((C .h A) +h B) -> (T` y) = (T` ((C .h A) +h B)))
43	42, 42	opreq12d 3973	. . . . . . . . . 10 |- (y = ((C .h A) +h B) -> ((T` y) .ih (T` y)) = ((T` ((C .h A) +h B)) .ih (T` ((C .h A) +h B))))
44		id 59	. . . . . . . . . . 11 |- (y = ((C .h A) +h B) -> y = ((C .h A) +h B))
45	44, 44	opreq12d 3973	. . . . . . . . . 10 |- (y = ((C .h A) +h B) -> (y .ih y) = (((C .h A) +h B) .ih ((C .h A) +h B)))
46	43, 45	eqeq12d 1487	. . . . . . . . 9 |- (y = ((C .h A) +h B) -> (((T` y) .ih (T` y)) = (y .ih y) <-> ((T` ((C .h A) +h B)) .ih (T` ((C .h A) +h B))) = (((C .h A) +h B) .ih ((C .h A) +h B))))
47	46	rcla4v 1870	. . . . . . . 8 |- (((C .h A) +h B) e. H~ -> (A.y e. H~ ((T` y) .ih (T` y)) = (y .ih y) -> ((T` ((C .h A) +h B)) .ih (T` ((C .h A) +h B))) = (((C .h A) +h B) .ih ((C .h A) +h B))))
48	41, 19, 47	mp2 43	. . . . . . 7 |- ((T` ((C .h A) +h B)) .ih (T` ((C .h A) +h B))) = (((C .h A) +h B) .ih ((C .h A) +h B))
49	9	lnopl 9849	. . . . . . . . . 10 |- ((C e. CC /\ A e. H~ /\ B e. H~) -> (T` ((C .h A) +h B)) = ((C .h (T` A)) +h (T` B)))
50	39, 1, 29, 49	mp3an 915	. . . . . . . . 9 |- (T` ((C .h A) +h B)) = ((C .h (T` A)) +h (T` B))
51	50, 50	opreq12i 3968	. . . . . . . 8 |- ((T` ((C .h A) +h B)) .ih (T` ((C .h A) +h B))) = (((C .h (T` A)) +h (T` B)) .ih ((C .h (T` A)) +h (T` B)))
52	10	ffvelrni 3810	. . . . . . . . . . 11 |- (A e. H~ -> (T` A) e. H~)
53	1, 52	ax-mp 7	. . . . . . . . . 10 |- (T` A) e. H~
54	39, 53	hvmulcl 8839	. . . . . . . . 9 |- (C .h (T` A)) e. H~
55	10	ffvelrni 3810	. . . . . . . . . 10 |- (B e. H~ -> (T` B) e. H~)
56	29, 55	ax-mp 7	. . . . . . . . 9 |- (T` B) e. H~
57	54, 56	hvaddcl 8843	. . . . . . . . 9 |- ((C .h (T` A)) +h (T` B)) e. H~
58		ax-his2 8905	. . . . . . . . 9 |- (((C .h (T` A)) e. H~ /\ (T` B) e. H~ /\ ((C .h (T` A)) +h (T` B)) e. H~) -> (((C .h (T` A)) +h (T` B)) .ih ((C .h (T` A)) +h (T` B))) = (((C .h (T