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 |
|
hvsubval |
|- ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H ) -> ( A -h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) ) |
5 |
3 4
|
sylan2 |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h ( -u 1 .h B ) ) = ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) ) |
6 |
|
hvm1neg |
|- ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h ( -u 1 .h B ) ) = ( -u -u 1 .h B ) ) |
7 |
1 6
|
mpan |
|- ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = ( -u -u 1 .h B ) ) |
8 |
|
negneg1e1 |
|- -u -u 1 = 1 |
9 |
8
|
oveq1i |
|- ( -u -u 1 .h B ) = ( 1 .h B ) |
10 |
7 9
|
eqtrdi |
|- ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = ( 1 .h B ) ) |
11 |
|
ax-hvmulid |
|- ( B e. ~H -> ( 1 .h B ) = B ) |
12 |
10 11
|
eqtrd |
|- ( B e. ~H -> ( -u 1 .h ( -u 1 .h B ) ) = B ) |
13 |
12
|
adantl |
|- ( ( A e. ~H /\ B e. ~H ) -> ( -u 1 .h ( -u 1 .h B ) ) = B ) |
14 |
13
|
oveq2d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h ( -u 1 .h ( -u 1 .h B ) ) ) = ( A +h B ) ) |
15 |
5 14
|
eqtr2d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) = ( A -h ( -u 1 .h B ) ) ) |