Theorem lnopunilem1

Description: Lemma for lnopunii . (Contributed by NM, 14-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	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	lnopunilem1	|- ( Re ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( C x. ( A .ih B ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnopunilem.1	|- T e. LinOp
2		lnopunilem.2	|- A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x )
3		lnopunilem.3	|- A e. ~H
4		lnopunilem.4	|- B e. ~H
5		lnopunilem1.5	|- C e. CC
6	1	lnopfi	|- T : ~H --> ~H
7	6	ffvelrni	|- ( A e. ~H -> ( T ` A ) e. ~H )
8	3 7	ax-mp	|- ( T ` A ) e. ~H
9	6	ffvelrni	|- ( B e. ~H -> ( T ` B ) e. ~H )
10	4 9	ax-mp	|- ( T ` B ) e. ~H
11	8 10	hicli	|- ( ( T ` A ) .ih ( T ` B ) ) e. CC
12	5 11	mulcli	|- ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) e. CC
13		reval	|- ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) e. CC -> ( Re ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) / 2 ) )
14	12 13	ax-mp	|- ( Re ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) / 2 )
15	3 4	hicli	|- ( A .ih B ) e. CC
16	5 15	mulcli	|- ( C x. ( A .ih B ) ) e. CC
17		reval	|- ( ( C x. ( A .ih B ) ) e. CC -> ( Re ` ( C x. ( A .ih B ) ) ) = ( ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) / 2 ) )
18	16 17	ax-mp	|- ( Re ` ( C x. ( A .ih B ) ) ) = ( ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) / 2 )
19		2fveq3	|- ( x = y -> ( normh ` ( T ` x ) ) = ( normh ` ( T ` y ) ) )
20		fveq2	|- ( x = y -> ( normh ` x ) = ( normh ` y ) )
21	19 20	eqeq12d	|- ( x = y -> ( ( normh ` ( T ` x ) ) = ( normh ` x ) <-> ( normh ` ( T ` y ) ) = ( normh ` y ) ) )
22	21	cbvralvw	|- ( A. x e. ~H ( normh ` ( T ` x ) ) = ( normh ` x ) <-> A. y e. ~H ( normh ` ( T ` y ) ) = ( normh ` y ) )
23	2 22	mpbi	|- A. y e. ~H ( normh ` ( T ` y ) ) = ( normh ` y )
24		oveq1	|- ( ( normh ` ( T ` y ) ) = ( normh ` y ) -> ( ( normh ` ( T ` y ) ) ^ 2 ) = ( ( normh ` y ) ^ 2 ) )
25	6	ffvelrni	|- ( y e. ~H -> ( T ` y ) e. ~H )
26		normsq	|- ( ( T ` y ) e. ~H -> ( ( normh ` ( T ` y ) ) ^ 2 ) = ( ( T ` y ) .ih ( T ` y ) ) )
27	25 26	syl	|- ( y e. ~H -> ( ( normh ` ( T ` y ) ) ^ 2 ) = ( ( T ` y ) .ih ( T ` y ) ) )
28		normsq	|- ( y e. ~H -> ( ( normh ` y ) ^ 2 ) = ( y .ih y ) )
29	27 28	eqeq12d	|- ( y e. ~H -> ( ( ( normh ` ( T ` y ) ) ^ 2 ) = ( ( normh ` y ) ^ 2 ) <-> ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) ) )
30	24 29	syl5ib	|- ( y e. ~H -> ( ( normh ` ( T ` y ) ) = ( normh ` y ) -> ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) ) )
31	30	ralimia	|- ( A. y e. ~H ( normh ` ( T ` y ) ) = ( normh ` y ) -> A. y e. ~H ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) )
32	23 31	ax-mp	|- A. y e. ~H ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y )
33		fveq2	|- ( y = A -> ( T ` y ) = ( T ` A ) )
34	33 33	oveq12d	|- ( y = A -> ( ( T ` y ) .ih ( T ` y ) ) = ( ( T ` A ) .ih ( T ` A ) ) )
35		id	|- ( y = A -> y = A )
36	35 35	oveq12d	|- ( y = A -> ( y .ih y ) = ( A .ih A ) )
37	34 36	eqeq12d	|- ( y = A -> ( ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) <-> ( ( T ` A ) .ih ( T ` A ) ) = ( A .ih A ) ) )
38	37	rspcv	|- ( A e. ~H -> ( A. y e. ~H ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) -> ( ( T ` A ) .ih ( T ` A ) ) = ( A .ih A ) ) )
39	3 32 38	mp2	|- ( ( T ` A ) .ih ( T ` A ) ) = ( A .ih A )
40	39	oveq2i	|- ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) = ( ( * ` C ) x. ( A .ih A ) )
41	40	oveq2i	|- ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) = ( C x. ( ( * ` C ) x. ( A .ih A ) ) )
42		fveq2	|- ( y = B -> ( T ` y ) = ( T ` B ) )
43	42 42	oveq12d	|- ( y = B -> ( ( T ` y ) .ih ( T ` y ) ) = ( ( T ` B ) .ih ( T ` B ) ) )
44		id	|- ( y = B -> y = B )
45	44 44	oveq12d	|- ( y = B -> ( y .ih y ) = ( B .ih B ) )
46	43 45	eqeq12d	|- ( y = B -> ( ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) <-> ( ( T ` B ) .ih ( T ` B ) ) = ( B .ih B ) ) )
47	46	rspcv	|- ( B e. ~H -> ( A. y e. ~H ( ( T ` y ) .ih ( T ` y ) ) = ( y .ih y ) -> ( ( T ` B ) .ih ( T ` B ) ) = ( B .ih B ) ) )
48	4 32 47	mp2	|- ( ( T ` B ) .ih ( T ` B ) ) = ( B .ih B )
49	41 48	oveq12i	|- ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) = ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih B ) )
50	49	oveq1i	|- ( ( ( 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 ) ) ) ) ) )
51	5	cjcli	|- ( * ` C ) e. CC
52	8 8	hicli	|- ( ( T ` A ) .ih ( T ` A ) ) e. CC
53	51 52	mulcli	|- ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) e. CC
54	5 53	mulcli	|- ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) e. CC
55	10 10	hicli	|- ( ( T ` B ) .ih ( T ` B ) ) e. CC
56	12	cjcli	|- ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) e. CC
57	54 55 12 56	add42i	|- ( ( ( 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. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) )
58	3 3	hicli	|- ( A .ih A ) e. CC
59	51 58	mulcli	|- ( ( * ` C ) x. ( A .ih A ) ) e. CC
60	5 59	mulcli	|- ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) e. CC
61	4 4	hicli	|- ( B .ih B ) e. CC
62	16	cjcli	|- ( * ` ( C x. ( A .ih B ) ) ) e. CC
63	60 61 16 62	add42i	|- ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih B ) ) + ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) ) = ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) ) + ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) ) )
64	5 3	hvmulcli	|- ( C .h A ) e. ~H
65	64 4	hvaddcli	|- ( ( C .h A ) +h B ) e. ~H
66		fveq2	|- ( y = ( ( C .h A ) +h B ) -> ( T ` y ) = ( T ` ( ( C .h A ) +h B ) ) )
67	66 66	oveq12d	|- ( y = ( ( C .h A ) +h B ) -> ( ( T ` y ) .ih ( T ` y ) ) = ( ( T ` ( ( C .h A ) +h B ) ) .ih ( T ` ( ( C .h A ) +h B ) ) ) )
68		id	|- ( y = ( ( C .h A ) +h B ) -> y = ( ( C .h A ) +h B ) )
69	68 68	oveq12d	|- ( y = ( ( C .h A ) +h B ) -> ( y .ih y ) = ( ( ( C .h A ) +h B ) .ih ( ( C .h A ) +h B ) ) )
70	67 69	eqeq12d	|- ( 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 ) ) ) )
71	70	rspcv	|- ( ( ( 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 ) ) ) )
72	65 32 71	mp2	|- ( ( T ` ( ( C .h A ) +h B ) ) .ih ( T ` ( ( C .h A ) +h B ) ) ) = ( ( ( C .h A ) +h B ) .ih ( ( C .h A ) +h B ) )
73		ax-his2	|- ( ( ( C .h A ) e. ~H /\ B e. ~H /\ ( ( C .h A ) +h B ) e. ~H ) -> ( ( ( C .h A ) +h B ) .ih ( ( C .h A ) +h B ) ) = ( ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) + ( B .ih ( ( C .h A ) +h B ) ) ) )
74	64 4 65 73	mp3an	|- ( ( ( C .h A ) +h B ) .ih ( ( C .h A ) +h B ) ) = ( ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) + ( B .ih ( ( C .h A ) +h B ) ) )
75		ax-his3	|- ( ( C e. CC /\ A e. ~H /\ ( ( C .h A ) +h B ) e. ~H ) -> ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) = ( C x. ( A .ih ( ( C .h A ) +h B ) ) ) )
76	5 3 65 75	mp3an	|- ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) = ( C x. ( A .ih ( ( C .h A ) +h B ) ) )
77		his7	|- ( ( A e. ~H /\ ( C .h A ) e. ~H /\ B e. ~H ) -> ( A .ih ( ( C .h A ) +h B ) ) = ( ( A .ih ( C .h A ) ) + ( A .ih B ) ) )
78	3 64 4 77	mp3an	|- ( A .ih ( ( C .h A ) +h B ) ) = ( ( A .ih ( C .h A ) ) + ( A .ih B ) )
79		his5	|- ( ( C e. CC /\ A e. ~H /\ A e. ~H ) -> ( A .ih ( C .h A ) ) = ( ( * ` C ) x. ( A .ih A ) ) )
80	5 3 3 79	mp3an	|- ( A .ih ( C .h A ) ) = ( ( * ` C ) x. ( A .ih A ) )
81	80	oveq1i	|- ( ( A .ih ( C .h A ) ) + ( A .ih B ) ) = ( ( ( * ` C ) x. ( A .ih A ) ) + ( A .ih B ) )
82	78 81	eqtri	|- ( A .ih ( ( C .h A ) +h B ) ) = ( ( ( * ` C ) x. ( A .ih A ) ) + ( A .ih B ) )
83	82	oveq2i	|- ( C x. ( A .ih ( ( C .h A ) +h B ) ) ) = ( C x. ( ( ( * ` C ) x. ( A .ih A ) ) + ( A .ih B ) ) )
84	5 59 15	adddii	|- ( C x. ( ( ( * ` C ) x. ( A .ih A ) ) + ( A .ih B ) ) ) = ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) )
85	76 83 84	3eqtri	|- ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) = ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) )
86		his7	|- ( ( B e. ~H /\ ( C .h A ) e. ~H /\ B e. ~H ) -> ( B .ih ( ( C .h A ) +h B ) ) = ( ( B .ih ( C .h A ) ) + ( B .ih B ) ) )
87	4 64 4 86	mp3an	|- ( B .ih ( ( C .h A ) +h B ) ) = ( ( B .ih ( C .h A ) ) + ( B .ih B ) )
88		his5	|- ( ( C e. CC /\ B e. ~H /\ A e. ~H ) -> ( B .ih ( C .h A ) ) = ( ( * ` C ) x. ( B .ih A ) ) )
89	5 4 3 88	mp3an	|- ( B .ih ( C .h A ) ) = ( ( * ` C ) x. ( B .ih A ) )
90	5 15	cjmuli	|- ( * ` ( C x. ( A .ih B ) ) ) = ( ( * ` C ) x. ( * ` ( A .ih B ) ) )
91	4 3	his1i	|- ( B .ih A ) = ( * ` ( A .ih B ) )
92	91	oveq2i	|- ( ( * ` C ) x. ( B .ih A ) ) = ( ( * ` C ) x. ( * ` ( A .ih B ) ) )
93	90 92	eqtr4i	|- ( * ` ( C x. ( A .ih B ) ) ) = ( ( * ` C ) x. ( B .ih A ) )
94	89 93	eqtr4i	|- ( B .ih ( C .h A ) ) = ( * ` ( C x. ( A .ih B ) ) )
95	94	oveq1i	|- ( ( B .ih ( C .h A ) ) + ( B .ih B ) ) = ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) )
96	87 95	eqtri	|- ( B .ih ( ( C .h A ) +h B ) ) = ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) )
97	85 96	oveq12i	|- ( ( ( C .h A ) .ih ( ( C .h A ) +h B ) ) + ( B .ih ( ( C .h A ) +h B ) ) ) = ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) ) + ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) ) )
98	72 74 97	3eqtrri	|- ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) ) + ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) ) ) = ( ( T ` ( ( C .h A ) +h B ) ) .ih ( T ` ( ( C .h A ) +h B ) ) )
99	1	lnopli	|- ( ( C e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( ( C .h A ) +h B ) ) = ( ( C .h ( T ` A ) ) +h ( T ` B ) ) )
100	5 3 4 99	mp3an	|- ( T ` ( ( C .h A ) +h B ) ) = ( ( C .h ( T ` A ) ) +h ( T ` B ) )
101	100 100	oveq12i	|- ( ( 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 ) ) )
102	5 8	hvmulcli	|- ( C .h ( T ` A ) ) e. ~H
103	102 10	hvaddcli	|- ( ( C .h ( T ` A ) ) +h ( T ` B ) ) e. ~H
104		ax-his2	|- ( ( ( 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 ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) + ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) ) )
105	102 10 103 104	mp3an	|- ( ( ( C .h ( T ` A ) ) +h ( T ` B ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) + ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) )
106	101 105	eqtri	|- ( ( T ` ( ( C .h A ) +h B ) ) .ih ( T ` ( ( C .h A ) +h B ) ) ) = ( ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) + ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) )
107		ax-his3	|- ( ( C e. CC /\ ( T ` A ) e. ~H /\ ( ( C .h ( T ` A ) ) +h ( T ` B ) ) e. ~H ) -> ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( C x. ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) ) )
108	5 8 103 107	mp3an	|- ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( C x. ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) )
109		his7	|- ( ( ( T ` A ) e. ~H /\ ( C .h ( T ` A ) ) e. ~H /\ ( T ` B ) e. ~H ) -> ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( T ` A ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) ) )
110	8 102 10 109	mp3an	|- ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( T ` A ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) )
111		his5	|- ( ( C e. CC /\ ( T ` A ) e. ~H /\ ( T ` A ) e. ~H ) -> ( ( T ` A ) .ih ( C .h ( T ` A ) ) ) = ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) )
112	5 8 8 111	mp3an	|- ( ( T ` A ) .ih ( C .h ( T ` A ) ) ) = ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) )
113	112	oveq1i	|- ( ( ( T ` A ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) ) = ( ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) )
114	110 113	eqtri	|- ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) )
115	114	oveq2i	|- ( C x. ( ( T ` A ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) ) = ( C x. ( ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) ) )
116	5 53 11	adddii	|- ( C x. ( ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) + ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) )
117	108 115 116	3eqtri	|- ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) )
118		his7	|- ( ( ( T ` B ) e. ~H /\ ( C .h ( T ` A ) ) e. ~H /\ ( T ` B ) e. ~H ) -> ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) )
119	10 102 10 118	mp3an	|- ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) )
120		his5	|- ( ( C e. CC /\ ( T ` B ) e. ~H /\ ( T ` A ) e. ~H ) -> ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) = ( ( * ` C ) x. ( ( T ` B ) .ih ( T ` A ) ) ) )
121	5 10 8 120	mp3an	|- ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) = ( ( * ` C ) x. ( ( T ` B ) .ih ( T ` A ) ) )
122	5 11	cjmuli	|- ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( ( * ` C ) x. ( * ` ( ( T ` A ) .ih ( T ` B ) ) ) )
123	10 8	his1i	|- ( ( T ` B ) .ih ( T ` A ) ) = ( * ` ( ( T ` A ) .ih ( T ` B ) ) )
124	123	oveq2i	|- ( ( * ` C ) x. ( ( T ` B ) .ih ( T ` A ) ) ) = ( ( * ` C ) x. ( * ` ( ( T ` A ) .ih ( T ` B ) ) ) )
125	122 124	eqtr4i	|- ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( ( * ` C ) x. ( ( T ` B ) .ih ( T ` A ) ) )
126	121 125	eqtr4i	|- ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) = ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) )
127	126	oveq1i	|- ( ( ( T ` B ) .ih ( C .h ( T ` A ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) = ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) )
128	119 127	eqtri	|- ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) = ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) )
129	117 128	oveq12i	|- ( ( ( C .h ( T ` A ) ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) + ( ( T ` B ) .ih ( ( C .h ( T ` A ) ) +h ( T ` B ) ) ) ) = ( ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) )
130	98 106 129	3eqtrri	|- ( ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) ) = ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( C x. ( A .ih B ) ) ) + ( ( * ` ( C x. ( A .ih B ) ) ) + ( B .ih B ) ) )
131	63 130	eqtr4i	|- ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih B ) ) + ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) ) = ( ( ( C x. ( ( * ` C ) x. ( ( T ` A ) .ih ( T ` A ) ) ) ) + ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) + ( ( T ` B ) .ih ( T ` B ) ) ) )
132	57 131	eqtr4i	|- ( ( ( 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. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) )
133	50 132	eqtr3i	|- ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih 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. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) )
134	60 61	addcli	|- ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih B ) ) e. CC
135	12 56	addcli	|- ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) e. CC
136	16 62	addcli	|- ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) e. CC
137	134 135 136	addcani	|- ( ( ( ( C x. ( ( * ` C ) x. ( A .ih A ) ) ) + ( B .ih 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. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) ) <-> ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) = ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) )
138	133 137	mpbi	|- ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) = ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) )
139	138	oveq1i	|- ( ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) / 2 ) = ( ( ( C x. ( A .ih B ) ) + ( * ` ( C x. ( A .ih B ) ) ) ) / 2 )
140	18 139	eqtr4i	|- ( Re ` ( C x. ( A .ih B ) ) ) = ( ( ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) + ( * ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) ) / 2 )
141	14 140	eqtr4i	|- ( Re ` ( C x. ( ( T ` A ) .ih ( T ` B ) ) ) ) = ( Re ` ( C x. ( A .ih B ) ) )