Theorem lnophmlem2

Description: Lemma for lnophmi . (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnophmlem.1	$$⊢A\in \mathscr{H}$$
	lnophmlem.2	$$⊢B\in \mathscr{H}$$
	lnophmlem.3	$$⊢T\in \mathrm{LinOp}$$
	lnophmlem.4	$$⊢\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(x\right)\in ℝ$$
Assertion	lnophmlem2	$$⊢A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B$$

Proof

Step	Hyp	Ref	Expression
1		lnophmlem.1	$$⊢A\in \mathscr{H}$$
2		lnophmlem.2	$$⊢B\in \mathscr{H}$$
3		lnophmlem.3	$$⊢T\in \mathrm{LinOp}$$
4		lnophmlem.4	$$⊢\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(x\right)\in ℝ$$
5	3	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
6	5	ffvelrni	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
7	1 6	ax-mp	$$⊢T\left(A\right)\in \mathscr{H}$$
8	5	ffvelrni	$$⊢B\in \mathscr{H}\to T\left(B\right)\in \mathscr{H}$$
9	2 8	ax-mp	$$⊢T\left(B\right)\in \mathscr{H}$$
10	2 7 1 9	polid2i	$$⊢B{\cdot }_{\mathrm{ih}}T\left(A\right)=\frac{\left(\left(B{+}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}T\left(A\right)\right)\right)-\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)\right)+\mathrm{i}\left(\left(\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)-\left(\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)\right)}{4}$$
11	2 1	hvcomi	$$⊢B{+}_{ℎ}A=A{+}_{ℎ}B$$
12	9 7	hvcomi	$$⊢T\left(B\right){+}_{ℎ}T\left(A\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$
13	3	lnopaddi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}B\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$
14	1 2 13	mp2an	$$⊢T\left(A{+}_{ℎ}B\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$
15	12 14	eqtr4i	$$⊢T\left(B\right){+}_{ℎ}T\left(A\right)=T\left(A{+}_{ℎ}B\right)$$
16	11 15	oveq12i	$$⊢\left(B{+}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}T\left(A\right)\right)=\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)$$
17	2 1 9 7	hisubcomi	$$⊢\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)$$
18	3	lnopsubi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{-}_{ℎ}B\right)=T\left(A\right){-}_{ℎ}T\left(B\right)$$
19	1 2 18	mp2an	$$⊢T\left(A{-}_{ℎ}B\right)=T\left(A\right){-}_{ℎ}T\left(B\right)$$
20	19	oveq2i	$$⊢\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)$$
21	17 20	eqtr4i	$$⊢\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)=\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)$$
22	16 21	oveq12i	$$⊢\left(\left(B{+}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}T\left(A\right)\right)\right)-\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)$$
23		ax-icn	$$⊢\mathrm{i}\in ℂ$$
24	23 2	hvmulcli	$$⊢\mathrm{i}{\cdot }_{ℎ}B\in \mathscr{H}$$
25	1 24	hvsubcli	$$⊢A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
26	5	ffvelrni	$$⊢A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}\to T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in \mathscr{H}$$
27	25 26	ax-mp	$$⊢T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in \mathscr{H}$$
28	23 23 25 27	his35i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right){\cdot }_{\mathrm{ih}}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}\bar{\mathrm{i}}\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
29	23 1 24	hvsubdistr1i	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
30	23 1	hvmulcli	$$⊢\mathrm{i}{\cdot }_{ℎ}A\in \mathscr{H}$$
31	23 24	hvmulcli	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
32	30 31	hvsubvali	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
33	23 23 2	hvmulassi	$$⊢\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B=\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)$$
34	33	oveq2i	$$⊢-1{\cdot }_{ℎ}\left(\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B\right)=-1{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
35		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
36	35	oveq2i	$$⊢-1\mathrm{i}\mathrm{i}=-1-1$$
37		ax-1cn	$$⊢1\in ℂ$$
38	37 37	mul2negi	$$⊢-1-1=1\cdot 1$$
39		1t1e1	$$⊢1\cdot 1=1$$
40	36 38 39	3eqtri	$$⊢-1\mathrm{i}\mathrm{i}=1$$
41	40	oveq1i	$$⊢-1\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B=1{\cdot }_{ℎ}B$$
42		neg1cn	$$⊢-1\in ℂ$$
43	23 23	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
44	42 43 2	hvmulassi	$$⊢-1\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B=-1{\cdot }_{ℎ}\left(\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B\right)$$
45		ax-hvmulid	$$⊢B\in \mathscr{H}\to 1{\cdot }_{ℎ}B=B$$
46	2 45	ax-mp	$$⊢1{\cdot }_{ℎ}B=B$$
47	41 44 46	3eqtr3i	$$⊢-1{\cdot }_{ℎ}\left(\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B\right)=B$$
48	34 47	eqtr3i	$$⊢-1{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=B$$
49	48	oveq2i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}B$$
50	32 49	eqtri	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}B$$
51	30 2	hvcomi	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}B=B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)$$
52	29 50 51	3eqtri	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)$$
53	52	fveq2i	$$⊢T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=T\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right)$$
54	3	lnopmuli	$$⊢\left(\mathrm{i}\in ℂ\wedge A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}\right)\to T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}{\cdot }_{ℎ}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
55	23 25 54	mp2an	$$⊢T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}{\cdot }_{ℎ}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
56	3	lnopaddmuli	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to T\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right)=T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)$$
57	23 2 1 56	mp3an	$$⊢T\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right)=T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)$$
58	53 55 57	3eqtr3i	$$⊢\mathrm{i}{\cdot }_{ℎ}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)$$
59	52 58	oveq12i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right){\cdot }_{\mathrm{ih}}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)$$
60		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
61	60	oveq2i	$$⊢\mathrm{i}\bar{\mathrm{i}}=\mathrm{i}\left(-\mathrm{i}\right)$$
62	23 23	mulneg2i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=-\mathrm{i}\mathrm{i}$$
63	35	negeqi	$$⊢-\mathrm{i}\mathrm{i}=--1$$
64		negneg1e1	$$⊢--1=1$$
65	63 64	eqtri	$$⊢-\mathrm{i}\mathrm{i}=1$$
66	61 62 65	3eqtri	$$⊢\mathrm{i}\bar{\mathrm{i}}=1$$
67	66	oveq1i	$$⊢\mathrm{i}\bar{\mathrm{i}}\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=1\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
68	25 1 3 4	lnophmlem1	$$⊢\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in ℝ$$
69	68	recni	$$⊢\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in ℂ$$
70	69	mulid2i	$$⊢1\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
71	67 70	eqtri	$$⊢\mathrm{i}\bar{\mathrm{i}}\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
72	28 59 71	3eqtr3i	$$⊢\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)=\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
73	23 7	hvmulcli	$$⊢\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\in \mathscr{H}$$
74	2 30 9 73	hisubcomi	$$⊢\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)=\left(\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right){-}_{ℎ}T\left(B\right)\right)$$
75	35	oveq1i	$$⊢\mathrm{i}\mathrm{i}{\cdot }_{ℎ}B=-1{\cdot }_{ℎ}B$$
76	33 75	eqtr3i	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)=-1{\cdot }_{ℎ}B$$
77	76	oveq2i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
78	23 1 24	hvdistr1i	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
79	30 2	hvsubvali	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B=\left(\mathrm{i}{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
80	77 78 79	3eqtr4i	$$⊢\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B$$
81	80	fveq2i	$$⊢T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=T\left(\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B\right)$$
82	1 24	hvaddcli	$$⊢A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}$$
83	3	lnopmuli	$$⊢\left(\mathrm{i}\in ℂ\wedge A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}\right)\to T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
84	23 82 83	mp2an	$$⊢T\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
85	3	lnopmulsubi	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B\right)=\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right){-}_{ℎ}T\left(B\right)$$
86	23 1 2 85	mp3an	$$⊢T\left(\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B\right)=\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right){-}_{ℎ}T\left(B\right)$$
87	81 84 86	3eqtr3i	$$⊢\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right){-}_{ℎ}T\left(B\right)$$
88	80 87	oveq12i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right){\cdot }_{\mathrm{ih}}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(\left(\mathrm{i}{\cdot }_{ℎ}A\right){-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right){-}_{ℎ}T\left(B\right)\right)$$
89	74 88	eqtr4i	$$⊢\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)=\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right){\cdot }_{\mathrm{ih}}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
90	5	ffvelrni	$$⊢A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\in \mathscr{H}\to T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in \mathscr{H}$$
91	82 90	ax-mp	$$⊢T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in \mathscr{H}$$
92	23 23 82 91	his35i	$$⊢\left(\mathrm{i}{\cdot }_{ℎ}\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right){\cdot }_{\mathrm{ih}}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\mathrm{i}\bar{\mathrm{i}}\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
93	66	oveq1i	$$⊢\mathrm{i}\bar{\mathrm{i}}\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=1\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
94	82 1 3 4	lnophmlem1	$$⊢\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in ℝ$$
95	94	recni	$$⊢\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in ℂ$$
96	95	mulid2i	$$⊢1\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
97	93 96	eqtri	$$⊢\mathrm{i}\bar{\mathrm{i}}\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
98	89 92 97	3eqtri	$$⊢\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)=\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)$$
99	72 98	oveq12i	$$⊢\left(\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)-\left(\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)=\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
100	99	oveq2i	$$⊢\mathrm{i}\left(\left(\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)-\left(\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)\right)=\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
101	22 100	oveq12i	$$⊢\left(\left(B{+}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}T\left(A\right)\right)\right)-\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)\right)+\mathrm{i}\left(\left(\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)-\left(\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
102	101	oveq1i	$$⊢\frac{\left(\left(B{+}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}T\left(A\right)\right)\right)-\left(\left(B{-}_{ℎ}A\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}T\left(A\right)\right)\right)+\mathrm{i}\left(\left(\left(B{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)-\left(\left(B{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}A\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(B\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(A\right)\right)\right)\right)\right)}{4}=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}$$
103	10 102	eqtri	$$⊢B{\cdot }_{\mathrm{ih}}T\left(A\right)=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}$$
104	103	fveq2i	$$⊢\overline{B{\cdot }_{\mathrm{ih}}T\left(A\right)}=\stackrel{‾}{\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}}$$
105		4ne0	$$⊢4\ne 0$$
106	1 2	hvaddcli	$$⊢A{+}_{ℎ}B\in \mathscr{H}$$
107	106 1 3 4	lnophmlem1	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\in ℝ$$
108	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
109	108 1 3 4	lnophmlem1	$$⊢\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\in ℝ$$
110	107 109	resubcli	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)\in ℝ$$
111	110	recni	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)\in ℂ$$
112	68 94	resubcli	$$⊢\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\in ℝ$$
113	112	recni	$$⊢\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\in ℂ$$
114	23 113	mulcli	$$⊢\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\in ℂ$$
115	111 114	addcli	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\in ℂ$$
116		4re	$$⊢4\in ℝ$$
117	116	recni	$$⊢4\in ℂ$$
118	115 117	cjdivi	$$⊢4\ne 0\to \stackrel{‾}{\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}}=\frac{\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}}{\bar{4}}$$
119	105 118	ax-mp	$$⊢\stackrel{‾}{\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}{4}}=\frac{\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}}{\bar{4}}$$
120		cjreim	$$⊢\left(\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)\in ℝ\wedge \left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\in ℝ\right)\to \overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
121	110 112 120	mp2an	$$⊢\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
122	82 2 3 4	lnophmlem1	$$⊢\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\in ℝ$$
123	68 122	resubcli	$$⊢\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\in ℝ$$
124	123	recni	$$⊢\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\in ℂ$$
125	23 124	mulcli	$$⊢\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\in ℂ$$
126	111 125	negsubi	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\left(-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
127	121 126	eqtr4i	$$⊢\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\left(-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\right)$$
128	23 113	mulneg2i	$$⊢\mathrm{i}\left(-\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\right)=-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
129	69 95	negsubdi2i	$$⊢-\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)=\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)$$
130	129	oveq2i	$$⊢\mathrm{i}\left(-\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\right)=\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
131	128 130	eqtr3i	$$⊢-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)=\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
132	131	oveq2i	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\left(-\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)$$
133	14	oveq2i	$$⊢\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)=\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)$$
134	133 20	oveq12i	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)$$
135	3	lnopaddmuli	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)$$
136	23 1 2 135	mp3an	$$⊢T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)$$
137	136	oveq2i	$$⊢\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)$$
138	3	lnopsubmuli	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)$$
139	23 1 2 138	mp3an	$$⊢T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)$$
140	139	oveq2i	$$⊢\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)=\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)$$
141	137 140	oveq12i	$$⊢\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)=\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)$$
142	141	oveq2i	$$⊢\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)=\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)$$
143	134 142	oveq12i	$$⊢\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)$$
144	127 132 143	3eqtri	$$⊢\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}=\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)$$
145		cjre	$$⊢4\in ℝ\to \bar{4}=4$$
146	116 145	ax-mp	$$⊢\bar{4}=4$$
147	144 146	oveq12i	$$⊢\frac{\overline{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}B\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}B\right)\right)+\mathrm{i}\left(\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)-\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}T\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right)\right)\right)}}{\bar{4}}=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)}{4}$$
148	104 119 147	3eqtrri	$$⊢\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)}{4}=\overline{B{\cdot }_{\mathrm{ih}}T\left(A\right)}$$
149	1 9 2 7	polid2i	$$⊢A{\cdot }_{\mathrm{ih}}T\left(B\right)=\frac{\left(\left(A{+}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}T\left(B\right)\right)\right)-\left(\left(A{-}_{ℎ}B\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}T\left(B\right)\right)\right)+\mathrm{i}\left(\left(\left(A{+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){+}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)-\left(\left(A{-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}B\right)\right){\cdot }_{\mathrm{ih}}\left(T\left(A\right){-}_{ℎ}\left(\mathrm{i}{\cdot }_{ℎ}T\left(B\right)\right)\right)\right)\right)}{4}$$
150	7 2	his1i	$$⊢T\left(A\right){\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}T\left(A\right)}$$
151	148 149 150	3eqtr4i	$$⊢A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B$$