Theorem lnophmlem2 9880

Description: Lemma for lnophm 9881. Warning: The HTML proof page is 1/2 megabyte in size.

Hypotheses

Ref	Expression
lnophmlem.1	|- A e. H~
lnophmlem.2	|- B e. H~
lnophmlem.3	|- T e. LinOp
lnophmlem.4	|- A.x e. H~ (x .ih (T` x)) e. RR

Assertion

Ref	Expression
lnophmlem2	|- (A .ih (T` B)) = ((T` A) .ih B)

Distinct variable groups:   x,A   x,B   x,T

Proof of Theorem lnophmlem2

Step	Hyp	Ref	Expression
1		lnophmlem.2	. . . . . 6 |- B e. H~
2		lnophmlem.1	. . . . . . 7 |- A e. H~
3		lnophmlem.3	. . . . . . . . 9 |- T e. LinOp
4	3	lnopf 9832	. . . . . . . 8 |- T:H~-->H~
5	4	ffvelrni 3806	. . . . . . 7 |- (A e. H~ -> (T` A) e. H~)
6	2, 5	ax-mp 7	. . . . . 6 |- (T` A) e. H~
7	4	ffvelrni 3806	. . . . . . 7 |- (B e. H~ -> (T` B) e. H~)
8	1, 7	ax-mp 7	. . . . . 6 |- (T` B) e. H~
9	1, 6, 2, 8	polid2 8963	. . . . 5 |- (B .ih (T` A)) = (((((B +h A) .ih ((T` B) +h (T` A))) - ((B -h A) .ih ((T` B) -h (T` A)))) + (i x. (((B +h (i .h A)) .ih ((T` B) +h (i .h (T` A)))) - ((B -h (i .h A)) .ih ((T` B) -h (i .h (T` A))))))) / 4)
10	1, 2	hvcom 8828	. . . . . . . . 9 |- (B +h A) = (A +h B)
11	8, 6	hvcom 8828	. . . . . . . . . 10 |- ((T` B) +h (T` A)) = ((T` A) +h (T` B))
12	3	lnopadd 9834	. . . . . . . . . . 11 |- ((A e. H~ /\ B e. H~) -> (T` (A +h B)) = ((T` A) +h (T` B)))
13	2, 1, 12	mp2an 696	. . . . . . . . . 10 |- (T` (A +h B)) = ((T` A) +h (T` B))
14	11, 13	eqtr4 1495	. . . . . . . . 9 |- ((T` B) +h (T` A)) = (T` (A +h B))
15	10, 14	opreq12i 3964	. . . . . . . 8 |- ((B +h A) .ih ((T` B) +h (T` A))) = ((A +h B) .ih (T` (A +h B)))
16	1, 2, 8, 6	hisubcom 8909	. . . . . . . . 9 |- ((B -h A) .ih ((T` B) -h (T` A))) = ((A -h B) .ih ((T` A) -h (T` B)))
17	3	lnopsub 9837	. . . . . . . . . . 11 |- ((A e. H~ /\ B e. H~) -> (T` (A -h B)) = ((T` A) -h (T` B)))
18	2, 1, 17	mp2an 696	. . . . . . . . . 10 |- (T` (A -h B)) = ((T` A) -h (T` B))
19	18	opreq2i 3963	. . . . . . . . 9 |- ((A -h B) .ih (T` (A -h B))) = ((A -h B) .ih ((T` A) -h (T` B)))
20	16, 19	eqtr4 1495	. . . . . . . 8 |- ((B -h A) .ih ((T` B) -h (T` A))) = ((A -h B) .ih (T` (A -h B)))
21	15, 20	opreq12i 3964	. . . . . . 7 |- (((B +h A) .ih ((T` B) +h (T` A))) - ((B -h A) .ih ((T` B) -h (T` A)))) = (((A +h B) .ih (T` (A +h B))) - ((A -h B) .ih (T` (A -h B))))
22		axicn 5250	. . . . . . . . . . . . 13 |- i e. CC
23	22, 1	hvmulcl 8823	. . . . . . . . . . . . 13 |- (i .h B) e. H~
24	22, 2, 23	hvsubdistr1 8858	. . . . . . . . . . . 12 |- (i .h (A -h (i .h B))) = ((i .h A) -h (i .h (i .h B)))
25	22, 2	hvmulcl 8823	. . . . . . . . . . . . . 14 |- (i .h A) e. H~
26	22, 23	hvmulcl 8823	. . . . . . . . . . . . . 14 |- (i .h (i .h B)) e. H~
27	25, 26	hvsubval 8829	. . . . . . . . . . . . 13 |- ((i .h A) -h (i .h (i .h B))) = ((i .h A) +h (-u1 .h (i .h (i .h B))))
28	22, 22, 1	hvmulass 8852	. . . . . . . . . . . . . . . 16 |- ((i x. i) .h B) = (i .h (i .h B))
29	28	opreq2i 3963	. . . . . . . . . . . . . . 15 |- (-u1 .h ((i x. i) .h B)) = (-u1 .h (i .h (i .h B)))
30		ixi 5662	. . . . . . . . . . . . . . . . . . 19 |- (i x. i) = -u1
31	30	opreq2i 3963	. . . . . . . . . . . . . . . . . 18 |- (-u1 x. (i x. i)) = (-u1 x. -u1)
32		ax1cn 5249	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
33	32, 32	mul2neg 5427	. . . . . . . . . . . . . . . . . 18 |- (-u1 x. -u1) = (1 x. 1)
34	32	mulid1 5312	. . . . . . . . . . . . . . . . . 18 |- (1 x. 1) = 1
35	31, 33, 34	3eqtr 1496	. . . . . . . . . . . . . . . . 17 |- (-u1 x. (i x. i)) = 1
36	35	opreq1i 3962	. . . . . . . . . . . . . . . 16 |- ((-u1 x. (i x. i)) .h B) = (1 .h B)
37	32	negcl 5349	. . . . . . . . . . . . . . . . 17 |- -u1 e. CC
38	22, 22	mulcl 5301	. . . . . . . . . . . . . . . . 17 |- (i x. i) e. CC
39	37, 38, 1	hvmulass 8852	. . . . . . . . . . . . . . . 16 |- ((-u1 x. (i x. i)) .h B) = (-u1 .h ((i x. i) .h B))
40		ax-hvmulid 8815	. . . . . . . . . . . . . . . . 17 |- (B e. H~ -> (1 .h B) = B)
41	1, 40	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (1 .h B) = B
42	36, 39, 41	3eqtr3 1500	. . . . . . . . . . . . . . 15 |- (-u1 .h ((i x. i) .h B)) = B
43	29, 42	eqtr3 1494	. . . . . . . . . . . . . 14 |- (-u1 .h (i .h (i .h B))) = B
44	43	opreq2i 3963	. . . . . . . . . . . . 13 |- ((i .h A) +h (-u1 .h (i .h (i .h B)))) = ((i .h A) +h B)
45	27, 44	eqtr 1492	. . . . . . . . . . . 12 |- ((i .h A) -h (i .h (i .h B))) = ((i .h A) +h B)
46	25, 1	hvcom 8828	. . . . . . . . . . . 12 |- ((i .h A) +h B) = (B +h (i .h A))
47	24, 45, 46	3eqtr 1496	. . . . . . . . . . 11 |- (i .h (A -h (i .h B))) = (B +h (i .h A))
48	47	fveq2i 3718	. . . . . . . . . . . 12 |- (T` (i .h (A -h (i .h B)))) = (T` (B +h (i .h A)))
49	2, 23	hvsubcl 8830	. . . . . . . . . . . . 13 |- (A -h (i .h B)) e. H~
50	3	lnopmul 9835	. . . . . . . . . . . . 13 |- ((i e. CC /\ (A -h (i .h B)) e. H~) -> (T` (i .h (A -h (i .h B)))) = (i .h (T` (A -h (i .h B)))))
51	22, 49, 50	mp2an 696	. . . . . . . . . . . 12 |- (T` (i .h (A -h (i .h B)))) = (i .h (T` (A -h (i .h B))))
52	3	lnopaddmul 9836	. . . . . . . . . . . . 13 |- ((i e. CC /\ B e. H~ /\ A e. H~) -> (T` (B +h (i .h A))) = ((T` B) +h (i .h (T` A))))
53	22, 1, 2, 52	mp3an 914	. . . . . . . . . . . 12 |- (T` (B +h (i .h A))) = ((T` B) +h (i .h (T` A)))
54	48, 51, 53	3eqtr3 1500	. . . . . . . . . . 11 |- (i .h (T` (A -h (i .h B)))) = ((T` B) +h (i .h (T` A)))
55	47, 54	opreq12i 3964	. . . . . . . . . 10 |- ((i .h (A -h (i .h B))) .ih (i .h (T` (A -h (i .h B))))) = ((B +h (i .h A)) .ih ((T` B) +h (i .h (T` A))))
56	4	ffvelrni 3806	. . . . . . . . . . . . 13 |- ((A -h (i .h B)) e. H~ -> (T` (A -h (i .h B))) e. H~)
57	49, 56	ax-mp 7	. . . . . . . . . . . 12 |- (T` (A -h (i .h B))) e. H~
58	22, 22, 49, 57	his35 8894	. . . . . . . . . . 11 |- ((i .h (A -h (i .h B))) .ih (i .h (T` (A -h (i .h B))))) = ((i x. (*` i)) x. ((A -h (i .h B)) .ih (T` (A -h (i .h B)))))
59		cji 6770	. . . . . . . . . . . . . 14 |- (*` i) = -ui
60	59	opreq2i 3963	. . . . . . . . . . . . 13 |- (i x. (*` i)) = (i x. -ui)
61	22, 22	mulneg2 5426	. . . . . . . . . . . . 13 |- (i x. -ui) = -u(i x. i)
62	30	negeqi 5340	. . . . . . . . . . . . . 14 |- -u(i x. i) = -u-u1
63	32	negneg 5370	. . . . . . . . . . . . . 14 |- -u-u1 = 1
64	62, 63	eqtr 1492	. . . . . . . . . . . . 13 |- -u(i x. i) = 1
65	60, 61, 64	3eqtr 1496	. . . . . . . . . . . 12 |- (i x. (*` i)) = 1
66	65	opreq1i 3962	. . . . . . . . . . 11 |- ((i x. (*` i)) x. ((A -h (i .h B)) .ih (T` (A -h (i .h B))))) = (1 x. ((A -h (i .h B)) .ih (T` (A -h (i .h B)))))
67		lnophmlem.4	. . . . . . . . . . . . . 14 |- A.x e. H~ (x .ih (T` x)) e. RR
68	49, 2, 3, 67	lnophmlem1 9879	. . . . . . . . . . . . 13 |- ((A -h (i .h B)) .ih (T` (A -h (i .h B)))) e. RR
69	68	recn 5294	. . . . . . . . . . . 12 |- ((A -h (i .h B)) .ih (T` (A -h (i .h B)))) e. CC
70	69	mulid2 5313	. . . . . . . . . . 11 |- (1 x. ((A -h (i .h B)) .ih (T` (A -h (i .h B))))) = ((A -h (i .h B)) .ih (T` (A -h (i .h B))))
71	58, 66, 70	3eqtr 1496	. . . . . . . . . 10 |- ((i .h (A -h (i .h B))) .ih (i .h (T` (A -h (i .h B))))) = ((A -h (i .h B)) .ih (T` (A -h (i .h B))))
72	55, 71	eqtr3 1494	. . . . . . . . 9 |- ((B +h (i .h A)) .ih ((T` B) +h (i .h (T` A)))) = ((A -h (i .h B)) .ih (T` (A -h (i .h B))))
73	22, 6	hvmulcl 8823	. . . . . . . . . . 11 |- (i .h (T` A)) e. H~
74	1, 25, 8, 73	hisubcom 8909	. . . . . . . . . 10 |- (