Step |
Hyp |
Ref |
Expression |
1 |
|
hvnegdi.1 |
|- A e. ~H |
2 |
|
hvnegdi.2 |
|- B e. ~H |
3 |
1 2
|
hvsubvali |
|- ( A -h B ) = ( A +h ( -u 1 .h B ) ) |
4 |
3
|
oveq2i |
|- ( ( A +h B ) +h ( A -h B ) ) = ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) |
5 |
|
neg1cn |
|- -u 1 e. CC |
6 |
5 2
|
hvmulcli |
|- ( -u 1 .h B ) e. ~H |
7 |
1 2 1 6
|
hvadd4i |
|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) ) |
8 |
|
hv2times |
|- ( A e. ~H -> ( 2 .h A ) = ( A +h A ) ) |
9 |
1 8
|
ax-mp |
|- ( 2 .h A ) = ( A +h A ) |
10 |
9
|
eqcomi |
|- ( A +h A ) = ( 2 .h A ) |
11 |
2
|
hvnegidi |
|- ( B +h ( -u 1 .h B ) ) = 0h |
12 |
10 11
|
oveq12i |
|- ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h ) |
13 |
7 12
|
eqtri |
|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h ) |
14 |
|
2cn |
|- 2 e. CC |
15 |
14 1
|
hvmulcli |
|- ( 2 .h A ) e. ~H |
16 |
|
ax-hvaddid |
|- ( ( 2 .h A ) e. ~H -> ( ( 2 .h A ) +h 0h ) = ( 2 .h A ) ) |
17 |
15 16
|
ax-mp |
|- ( ( 2 .h A ) +h 0h ) = ( 2 .h A ) |
18 |
13 17
|
eqtri |
|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( 2 .h A ) |
19 |
4 18
|
eqtri |
|- ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A ) |