Theorem homco2t 9901

Description: Move a scalar product out of a composition of operators. The operator T must be linear, unlike homco1t 9727 that works for any operators.

Assertion

Ref	Expression
homco2t	|- ((A e. CC /\ T e. LinOp /\ U:H~-->H~) -> (T o. (A .op U)) = (A .op (T o. U)))

Proof of Theorem homco2t

Step	Hyp	Ref	Expression
1		lnopmult 9891	. . . . . . . . 9 |- ((T e. LinOp /\ A e. CC /\ (U` x) e. H~) -> (T` (A .h (U` x))) = (A .h (T` (U` x))))
2		ffvelrn 3814	. . . . . . . . 9 |- ((U:H~-->H~ /\ x e. H~) -> (U` x) e. H~)
3	1, 2	syl3an3 861	. . . . . . . 8 |- ((T e. LinOp /\ A e. CC /\ (U:H~-->H~ /\ x e. H~)) -> (T` (A .h (U` x))) = (A .h (T` (U` x))))
4	3	3exp 832	. . . . . . 7 |- (T e. LinOp -> (A e. CC -> ((U:H~-->H~ /\ x e. H~) -> (T` (A .h (U` x))) = (A .h (T` (U` x))))))
5	4	exp4a 378	. . . . . 6 |- (T e. LinOp -> (A e. CC -> (U:H~-->H~ -> (x e. H~ -> (T` (A .h (U` x))) = (A .h (T` (U` x)))))))
6	5	com12 11	. . . . 5 |- (A e. CC -> (T e. LinOp -> (U:H~-->H~ -> (x e. H~ -> (T` (A .h (U` x))) = (A .h (T` (U` x)))))))
7	6	3imp1 846	. . . 4 |- (((A e. CC /\ T e. LinOp /\ U:H~-->H~) /\ x e. H~) -> (T` (A .h (U` x))) = (A .h (T` (U` x))))
8		fvco3 3776	. . . . . . . . . . . 12 |- ((Fun T /\ (A .op U):H~-->H~ /\ x e. H~) -> ((T o. (A .op U))` x) = (T` ((A .op U)` x)))
9		ffun 3629	. . . . . . . . . . . 12 |- (T:H~-->H~ -> Fun T)
10	8, 9	syl3an1 859	. . . . . . . . . . 11 |- ((T:H~-->H~ /\ (A .op U):H~-->H~ /\ x e. H~) -> ((T o. (A .op U))` x) = (T` ((A .op U)` x)))
11		homulclt 9685	. . . . . . . . . . 11 |- ((A e. CC /\ U:H~-->H~) -> (A .op U):H~-->H~)
12	10, 11	syl3an2 860	. . . . . . . . . 10 |- ((T:H~-->H~ /\ (A e. CC /\ U:H~-->H~) /\ x e. H~) -> ((T o. (A .op U))` x) = (T` ((A .op U)` x)))
13	12	3exp 832	. . . . . . . . 9 |- (T:H~-->H~ -> ((A e. CC /\ U:H~-->H~) -> (x e. H~ -> ((T o. (A .op U))` x) = (T` ((A .op U)` x)))))
14	13	exp3a 375	. . . . . . . 8 |- (T:H~-->H~ -> (A e. CC -> (U:H~-->H~ -> (x e. H~ -> ((T o. (A .op U))` x) = (T` ((A .op U)` x))))))
15	14	com12 11	. . . . . . 7 |- (A e. CC -> (T:H~-->H~ -> (U:H~-->H~ -> (x e. H~ -> ((T o. (A .op U))` x) = (T` ((A .op U)` x))))))
16	15	3imp1 846	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((T o. (A .op U))` x) = (T` ((A .op U)` x)))
17		homvalt 9518	. . . . . . . . 9 |- ((A e. CC /\ U:H~-->H~ /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
18	17	3expa 833	. . . . . . . 8 |- (((A e. CC /\ U:H~-->H~) /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
19	18	3adantl2 804	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
20	19	fveq2d 3728	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (T` ((A .op U)` x)) = (T` (A .h (U` x))))
21	16, 20	eqtrd 1507	. . . . 5 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((T o. (A .op U))` x) = (T` (A .h (U` x))))
22		lnopft 9785	. . . . 5 |- (T e. LinOp -> T:H~-->H~)
23	21, 22	syl3anl2 874	. . . 4 |- (((A e. CC /\ T e. LinOp /\ U:H~-->H~) /\ x e. H~) -> ((T o. (A .op U))` x) = (T` (A .h (U` x))))
24		homvalt 9518	. . . . . . . . . 10 |- ((A e. CC /\ (T o. U):H~-->H~ /\ x e. H~) -> ((A .op (T o. U))` x) = (A .h ((T o. U)` x)))
25		fco 3636	. . . . . . . . . 10 |- ((T:H~-->H~ /\ U:H~-->H~) -> (T o. U):H~-->H~)
26	24, 25	syl3an2 860	. . . . . . . . 9 |- ((A e. CC /\ (T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T o. U))` x) = (A .h ((T o. U)` x)))
27	26	3expia 835	. . . . . . . 8 |- ((A e. CC /\ (T:H~-->H~ /\ U:H~-->H~)) -> (x e. H~ -> ((A .op (T o. U))` x) = (A .h ((T o. U)` x))))
28	27	3impb 829	. . . . . . 7 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (x e. H~ -> ((A .op (T o. U))` x) = (A .h ((T o. U)` x))))
29	28	imp 350	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T o. U))` x) = (A .h ((T o. U)` x)))
30		fvco3 3776	. . . . . . . . . 10 |- ((Fun T /\ U:H~-->H~ /\ x e. H~) -> ((T o. U)` x) = (T` (U` x)))
31	30, 9	syl3an1 859	. . . . . . . . 9 |- ((T:H~-->H~ /\ U:H~-->H~ /\ x e. H~) -> ((T o. U)` x) = (T` (U` x)))
32	31	3expa 833	. . . . . . . 8 |- (((T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((T o. U)` x) = (T` (U` x)))
33	32	opreq2d 3976	. . . . . . 7 |- (((T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T o. U)` x)) = (A .h (T` (U` x))))
34	33	3adantl1 803	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T o. U)` x)) = (A .h (T` (U` x))))
35	29, 34	eqtrd 1507	. . . . 5 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T o. U))` x) = (A .h (T` (U` x))))
36	35, 22	syl3anl2 874	. . . 4 |- (((A e. CC /\ T e. LinOp /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T o. U))` x) = (A .h (T` (U` x))))
37	7, 23, 36	3eqtr4d 1517	. . 3 |- (((A e. CC /\ T e. LinOp /\ U:H~-->H~) /\ x e. H~) -> ((T o. (A .op U))` x) = ((A .op (T o. U))` x))
38	37	r19.21aiva 1714	. 2 |- ((A e. CC /\ T e. LinOp /\ U:H~-->H~) -> A.x e. H~ ((T o. (A .op U))` x) = ((A .op (T o. U))` x))
39		hoeqt 9686	. . . 4 |- (((T o. (A .op U)):H~-->H~ /\ (A .op (T o. U)):H~-->H~) -> (A.x e. H~ ((T o. (A .op U))` x) = ((A .op (T o. U))` x) <-> (T o. (A .op U)) = (A .op (T o. U))))
40		fco 3636	. . . . . . 7 |- ((T:H~-->H~ /\ (A .op U):H~-->H~) -> (T o. (A .op U)):H~-->H~)
41	40, 11	sylan2 451	. . . . . 6 |- ((T:H~-->H~ /\ (A e. CC /\ U:H~-->H~)) -> (T o. (A .op U)):H~-->H~)
42	41	3impb 829	. . . . 5 |- ((T:H~-->H~ /\ A e. CC /\ U:H~-->H~) -> (T o. (A .op U)):H~-->H~)
43	42	3com12 837	. . . 4 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (T o. (A .op U)):H~-->H~)
44		homulclt 9685	. . . . . 6 |- ((A e. CC /\ (T o. U):H~-->H~) -> (A .op (T o. U)):H~-->H~)
45	44, 25	sylan2 451	. . . . 5 |- ((A e. CC /\ (T:H~