Step |
Hyp |
Ref |
Expression |
1 |
|
hods.1 |
|- R : ~H --> ~H |
2 |
|
hods.2 |
|- S : ~H --> ~H |
3 |
|
hods.3 |
|- T : ~H --> ~H |
4 |
1 2
|
hoaddcli |
|- ( R +op S ) : ~H --> ~H |
5 |
4 3
|
hocoi |
|- ( x e. ~H -> ( ( ( R +op S ) o. T ) ` x ) = ( ( R +op S ) ` ( T ` x ) ) ) |
6 |
1 3
|
hocofi |
|- ( R o. T ) : ~H --> ~H |
7 |
2 3
|
hocofi |
|- ( S o. T ) : ~H --> ~H |
8 |
|
hosval |
|- ( ( ( R o. T ) : ~H --> ~H /\ ( S o. T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) ) |
9 |
6 7 8
|
mp3an12 |
|- ( x e. ~H -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) ) |
10 |
3
|
ffvelrni |
|- ( x e. ~H -> ( T ` x ) e. ~H ) |
11 |
|
hosval |
|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ ( T ` x ) e. ~H ) -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) ) |
12 |
1 2 11
|
mp3an12 |
|- ( ( T ` x ) e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) ) |
13 |
10 12
|
syl |
|- ( x e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) ) |
14 |
1 3
|
hocoi |
|- ( x e. ~H -> ( ( R o. T ) ` x ) = ( R ` ( T ` x ) ) ) |
15 |
2 3
|
hocoi |
|- ( x e. ~H -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) ) |
16 |
14 15
|
oveq12d |
|- ( x e. ~H -> ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) ) |
17 |
13 16
|
eqtr4d |
|- ( x e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) ) |
18 |
9 17
|
eqtr4d |
|- ( x e. ~H -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( R +op S ) ` ( T ` x ) ) ) |
19 |
5 18
|
eqtr4d |
|- ( x e. ~H -> ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x ) ) |
20 |
19
|
rgen |
|- A. x e. ~H ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x ) |
21 |
4 3
|
hocofi |
|- ( ( R +op S ) o. T ) : ~H --> ~H |
22 |
6 7
|
hoaddcli |
|- ( ( R o. T ) +op ( S o. T ) ) : ~H --> ~H |
23 |
21 22
|
hoeqi |
|- ( A. x e. ~H ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x ) <-> ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. T ) ) ) |
24 |
20 23
|
mpbi |
|- ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. T ) ) |