Step |
Hyp |
Ref |
Expression |
1 |
|
neg1cn |
|- -u 1 e. CC |
2 |
|
hvmulcl |
|- ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H ) |
3 |
1 2
|
mpan |
|- ( B e. ~H -> ( -u 1 .h B ) e. ~H ) |
4 |
|
hvaddsubass |
|- ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) -h C ) = ( A +h ( ( -u 1 .h B ) -h C ) ) ) |
5 |
3 4
|
syl3an2 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) -h C ) = ( A +h ( ( -u 1 .h B ) -h C ) ) ) |
6 |
|
hvsubval |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) ) |
7 |
6
|
3adant3 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) ) |
8 |
7
|
oveq1d |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( ( A +h ( -u 1 .h B ) ) -h C ) ) |
9 |
|
simp1 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> A e. ~H ) |
10 |
|
hvaddcl |
|- ( ( B e. ~H /\ C e. ~H ) -> ( B +h C ) e. ~H ) |
11 |
10
|
3adant1 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( B +h C ) e. ~H ) |
12 |
|
hvsubval |
|- ( ( A e. ~H /\ ( B +h C ) e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) ) |
13 |
9 11 12
|
syl2anc |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) ) |
14 |
|
hvsubval |
|- ( ( ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
15 |
3 14
|
sylan |
|- ( ( B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
16 |
15
|
3adant1 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
17 |
|
ax-hvdistr1 |
|- ( ( -u 1 e. CC /\ B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
18 |
1 17
|
mp3an1 |
|- ( ( B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
19 |
18
|
3adant1 |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( -u 1 .h ( B +h C ) ) = ( ( -u 1 .h B ) +h ( -u 1 .h C ) ) ) |
20 |
16 19
|
eqtr4d |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) -h C ) = ( -u 1 .h ( B +h C ) ) ) |
21 |
20
|
oveq2d |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A +h ( ( -u 1 .h B ) -h C ) ) = ( A +h ( -u 1 .h ( B +h C ) ) ) ) |
22 |
13 21
|
eqtr4d |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A -h ( B +h C ) ) = ( A +h ( ( -u 1 .h B ) -h C ) ) ) |
23 |
5 8 22
|
3eqtr4d |
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) ) |