Step |
Hyp |
Ref |
Expression |
1 |
|
honegdi |
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T +op U ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) |
2 |
1
|
adantl |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( -u 1 .op ( T +op U ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) |
3 |
2
|
oveq2d |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) ) |
4 |
|
neg1cn |
|- -u 1 e. CC |
5 |
|
homulcl |
|- ( ( -u 1 e. CC /\ T : ~H --> ~H ) -> ( -u 1 .op T ) : ~H --> ~H ) |
6 |
4 5
|
mpan |
|- ( T : ~H --> ~H -> ( -u 1 .op T ) : ~H --> ~H ) |
7 |
|
homulcl |
|- ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H ) |
8 |
4 7
|
mpan |
|- ( U : ~H --> ~H -> ( -u 1 .op U ) : ~H --> ~H ) |
9 |
6 8
|
anim12i |
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( -u 1 .op T ) : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) ) |
10 |
|
hoadd4 |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( ( -u 1 .op T ) : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) ) -> ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) ) |
11 |
9 10
|
sylan2 |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( ( -u 1 .op T ) +op ( -u 1 .op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) ) |
12 |
3 11
|
eqtrd |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) ) |
13 |
|
hoaddcl |
|- ( ( R : ~H --> ~H /\ S : ~H --> ~H ) -> ( R +op S ) : ~H --> ~H ) |
14 |
|
hoaddcl |
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op U ) : ~H --> ~H ) |
15 |
|
honegsub |
|- ( ( ( R +op S ) : ~H --> ~H /\ ( T +op U ) : ~H --> ~H ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) -op ( T +op U ) ) ) |
16 |
13 14 15
|
syl2an |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) +op ( -u 1 .op ( T +op U ) ) ) = ( ( R +op S ) -op ( T +op U ) ) ) |
17 |
|
honegsub |
|- ( ( R : ~H --> ~H /\ T : ~H --> ~H ) -> ( R +op ( -u 1 .op T ) ) = ( R -op T ) ) |
18 |
17
|
ad2ant2r |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( R +op ( -u 1 .op T ) ) = ( R -op T ) ) |
19 |
|
honegsub |
|- ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( S +op ( -u 1 .op U ) ) = ( S -op U ) ) |
20 |
19
|
ad2ant2l |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( S +op ( -u 1 .op U ) ) = ( S -op U ) ) |
21 |
18 20
|
oveq12d |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op ( -u 1 .op T ) ) +op ( S +op ( -u 1 .op U ) ) ) = ( ( R -op T ) +op ( S -op U ) ) ) |
22 |
12 16 21
|
3eqtr3d |
|- ( ( ( R : ~H --> ~H /\ S : ~H --> ~H ) /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( ( R +op S ) -op ( T +op U ) ) = ( ( R -op T ) +op ( S -op U ) ) ) |