Theorem hoddii

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoddi.1	|- R e. LinOp
	hoddi.2	|- S : ~H --> ~H
	hoddi.3	|- T : ~H --> ~H
Assertion	hoddii	|- ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) )

Proof

Step	Hyp	Ref	Expression
1		hoddi.1	|- R e. LinOp
2		hoddi.2	|- S : ~H --> ~H
3		hoddi.3	|- T : ~H --> ~H
4	2	ffvelrni	|- ( x e. ~H -> ( S ` x ) e. ~H )
5	3	ffvelrni	|- ( x e. ~H -> ( T ` x ) e. ~H )
6	1	lnopsubi	|- ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( R ` ( ( S ` x ) -h ( T ` x ) ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )
7	4 5 6	syl2anc	|- ( x e. ~H -> ( R ` ( ( S ` x ) -h ( T ` x ) ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )
8		hodval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )
9	2 3 8	mp3an12	|- ( x e. ~H -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )
10	9	fveq2d	|- ( x e. ~H -> ( R ` ( ( S -op T ) ` x ) ) = ( R ` ( ( S ` x ) -h ( T ` x ) ) ) )
11	1	lnopfi	|- R : ~H --> ~H
12	11 2	hocoi	|- ( x e. ~H -> ( ( R o. S ) ` x ) = ( R ` ( S ` x ) ) )
13	11 3	hocoi	|- ( x e. ~H -> ( ( R o. T ) ` x ) = ( R ` ( T ` x ) ) )
14	12 13	oveq12d	|- ( x e. ~H -> ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )
15	7 10 14	3eqtr4d	|- ( x e. ~H -> ( R ` ( ( S -op T ) ` x ) ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )
16	2 3	hosubcli	|- ( S -op T ) : ~H --> ~H
17	11 16	hocoi	|- ( x e. ~H -> ( ( R o. ( S -op T ) ) ` x ) = ( R ` ( ( S -op T ) ` x ) ) )
18	11 2	hocofi	|- ( R o. S ) : ~H --> ~H
19	11 3	hocofi	|- ( R o. T ) : ~H --> ~H
20		hodval	|- ( ( ( R o. S ) : ~H --> ~H /\ ( R o. T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( R o. S ) -op ( R o. T ) ) ` x ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )
21	18 19 20	mp3an12	|- ( x e. ~H -> ( ( ( R o. S ) -op ( R o. T ) ) ` x ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )
22	15 17 21	3eqtr4d	|- ( x e. ~H -> ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x ) )
23	22	rgen	|- A. x e. ~H ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x )
24	11 16	hocofi	|- ( R o. ( S -op T ) ) : ~H --> ~H
25	18 19	hosubcli	|- ( ( R o. S ) -op ( R o. T ) ) : ~H --> ~H
26	24 25	hoeqi	|- ( A. x e. ~H ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x ) <-> ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) )
27	23 26	mpbi	|- ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) )