Step 
Hyp 
Ref 
Expression 
1 

hods.1 
 R : ~H > ~H 
2 

hods.2 
 S : ~H > ~H 
3 

hods.3 
 T : ~H > ~H 
4 
1

ffvelrni 
 ( x e. ~H > ( R ` x ) e. ~H ) 
5 
2

ffvelrni 
 ( x e. ~H > ( S ` x ) e. ~H ) 
6 
3

ffvelrni 
 ( x e. ~H > ( T ` x ) e. ~H ) 
7 

hvsubadd 
 ( ( ( R ` x ) e. ~H /\ ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) > ( ( ( R ` x ) h ( S ` x ) ) = ( T ` x ) <> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) ) 
8 
4 5 6 7

syl3anc 
 ( x e. ~H > ( ( ( R ` x ) h ( S ` x ) ) = ( T ` x ) <> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) ) 
9 

hodval 
 ( ( R : ~H > ~H /\ S : ~H > ~H /\ x e. ~H ) > ( ( R op S ) ` x ) = ( ( R ` x ) h ( S ` x ) ) ) 
10 
1 2 9

mp3an12 
 ( x e. ~H > ( ( R op S ) ` x ) = ( ( R ` x ) h ( S ` x ) ) ) 
11 
10

eqeq1d 
 ( x e. ~H > ( ( ( R op S ) ` x ) = ( T ` x ) <> ( ( R ` x ) h ( S ` x ) ) = ( T ` x ) ) ) 
12 

hosval 
 ( ( S : ~H > ~H /\ T : ~H > ~H /\ x e. ~H ) > ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) ) 
13 
2 3 12

mp3an12 
 ( x e. ~H > ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) ) 
14 
13

eqeq1d 
 ( x e. ~H > ( ( ( S +op T ) ` x ) = ( R ` x ) <> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) ) 
15 
8 11 14

3bitr4d 
 ( x e. ~H > ( ( ( R op S ) ` x ) = ( T ` x ) <> ( ( S +op T ) ` x ) = ( R ` x ) ) ) 
16 
15

ralbiia 
 ( A. x e. ~H ( ( R op S ) ` x ) = ( T ` x ) <> A. x e. ~H ( ( S +op T ) ` x ) = ( R ` x ) ) 
17 
1 2

hosubcli 
 ( R op S ) : ~H > ~H 
18 
17 3

hoeqi 
 ( A. x e. ~H ( ( R op S ) ` x ) = ( T ` x ) <> ( R op S ) = T ) 
19 
2 3

hoaddcli 
 ( S +op T ) : ~H > ~H 
20 
19 1

hoeqi 
 ( A. x e. ~H ( ( S +op T ) ` x ) = ( R ` x ) <> ( S +op T ) = R ) 
21 
16 18 20

3bitr3i 
 ( ( R op S ) = T <> ( S +op T ) = R ) 