Step |
Hyp |
Ref |
Expression |
1 |
|
hvaddcl |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H ) |
2 |
|
hvaddcl |
|- ( ( C e. ~H /\ D e. ~H ) -> ( C +h D ) e. ~H ) |
3 |
|
hvsubval |
|- ( ( ( A +h B ) e. ~H /\ ( C +h D ) e. ~H ) -> ( ( A +h B ) -h ( C +h D ) ) = ( ( A +h B ) +h ( -u 1 .h ( C +h D ) ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) -h ( C +h D ) ) = ( ( A +h B ) +h ( -u 1 .h ( C +h D ) ) ) ) |
5 |
|
hvsubval |
|- ( ( A e. ~H /\ C e. ~H ) -> ( A -h C ) = ( A +h ( -u 1 .h C ) ) ) |
6 |
5
|
ad2ant2r |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A -h C ) = ( A +h ( -u 1 .h C ) ) ) |
7 |
|
hvsubval |
|- ( ( B e. ~H /\ D e. ~H ) -> ( B -h D ) = ( B +h ( -u 1 .h D ) ) ) |
8 |
7
|
ad2ant2l |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( B -h D ) = ( B +h ( -u 1 .h D ) ) ) |
9 |
6 8
|
oveq12d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A -h C ) +h ( B -h D ) ) = ( ( A +h ( -u 1 .h C ) ) +h ( B +h ( -u 1 .h D ) ) ) ) |
10 |
|
neg1cn |
|- -u 1 e. CC |
11 |
|
ax-hvdistr1 |
|- ( ( -u 1 e. CC /\ C e. ~H /\ D e. ~H ) -> ( -u 1 .h ( C +h D ) ) = ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) |
12 |
10 11
|
mp3an1 |
|- ( ( C e. ~H /\ D e. ~H ) -> ( -u 1 .h ( C +h D ) ) = ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) |
13 |
12
|
adantl |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( -u 1 .h ( C +h D ) ) = ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) |
14 |
13
|
oveq2d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) +h ( -u 1 .h ( C +h D ) ) ) = ( ( A +h B ) +h ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) ) |
15 |
|
hvmulcl |
|- ( ( -u 1 e. CC /\ C e. ~H ) -> ( -u 1 .h C ) e. ~H ) |
16 |
10 15
|
mpan |
|- ( C e. ~H -> ( -u 1 .h C ) e. ~H ) |
17 |
16
|
anim2i |
|- ( ( A e. ~H /\ C e. ~H ) -> ( A e. ~H /\ ( -u 1 .h C ) e. ~H ) ) |
18 |
|
hvmulcl |
|- ( ( -u 1 e. CC /\ D e. ~H ) -> ( -u 1 .h D ) e. ~H ) |
19 |
10 18
|
mpan |
|- ( D e. ~H -> ( -u 1 .h D ) e. ~H ) |
20 |
19
|
anim2i |
|- ( ( B e. ~H /\ D e. ~H ) -> ( B e. ~H /\ ( -u 1 .h D ) e. ~H ) ) |
21 |
17 20
|
anim12i |
|- ( ( ( A e. ~H /\ C e. ~H ) /\ ( B e. ~H /\ D e. ~H ) ) -> ( ( A e. ~H /\ ( -u 1 .h C ) e. ~H ) /\ ( B e. ~H /\ ( -u 1 .h D ) e. ~H ) ) ) |
22 |
21
|
an4s |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A e. ~H /\ ( -u 1 .h C ) e. ~H ) /\ ( B e. ~H /\ ( -u 1 .h D ) e. ~H ) ) ) |
23 |
|
hvadd4 |
|- ( ( ( A e. ~H /\ ( -u 1 .h C ) e. ~H ) /\ ( B e. ~H /\ ( -u 1 .h D ) e. ~H ) ) -> ( ( A +h ( -u 1 .h C ) ) +h ( B +h ( -u 1 .h D ) ) ) = ( ( A +h B ) +h ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) ) |
24 |
22 23
|
syl |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h ( -u 1 .h C ) ) +h ( B +h ( -u 1 .h D ) ) ) = ( ( A +h B ) +h ( ( -u 1 .h C ) +h ( -u 1 .h D ) ) ) ) |
25 |
14 24
|
eqtr4d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) +h ( -u 1 .h ( C +h D ) ) ) = ( ( A +h ( -u 1 .h C ) ) +h ( B +h ( -u 1 .h D ) ) ) ) |
26 |
9 25
|
eqtr4d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A -h C ) +h ( B -h D ) ) = ( ( A +h B ) +h ( -u 1 .h ( C +h D ) ) ) ) |
27 |
4 26
|
eqtr4d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) -h ( C +h D ) ) = ( ( A -h C ) +h ( B -h D ) ) ) |