Step |
Hyp |
Ref |
Expression |
1 |
|
hvaddcl |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ~H ) |
2 |
1
|
adantr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A +h B ) e. ~H ) |
3 |
|
hvaddcl |
|- ( ( C e. ~H /\ D e. ~H ) -> ( C +h D ) e. ~H ) |
4 |
3
|
adantl |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C +h D ) e. ~H ) |
5 |
|
hvaddcl |
|- ( ( C e. ~H /\ B e. ~H ) -> ( C +h B ) e. ~H ) |
6 |
5
|
ancoms |
|- ( ( B e. ~H /\ C e. ~H ) -> ( C +h B ) e. ~H ) |
7 |
6
|
ad2ant2lr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C +h B ) e. ~H ) |
8 |
|
hvsubcan2 |
|- ( ( ( A +h B ) e. ~H /\ ( C +h D ) e. ~H /\ ( C +h B ) e. ~H ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A +h B ) = ( C +h D ) ) ) |
9 |
2 4 7 8
|
syl3anc |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A +h B ) = ( C +h D ) ) ) |
10 |
|
simpr |
|- ( ( A e. ~H /\ B e. ~H ) -> B e. ~H ) |
11 |
10
|
anim2i |
|- ( ( C e. ~H /\ ( A e. ~H /\ B e. ~H ) ) -> ( C e. ~H /\ B e. ~H ) ) |
12 |
11
|
ancoms |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( C e. ~H /\ B e. ~H ) ) |
13 |
|
hvsub4 |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ B e. ~H ) ) -> ( ( A +h B ) -h ( C +h B ) ) = ( ( A -h C ) +h ( B -h B ) ) ) |
14 |
12 13
|
syldan |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A +h B ) -h ( C +h B ) ) = ( ( A -h C ) +h ( B -h B ) ) ) |
15 |
|
hvsubid |
|- ( B e. ~H -> ( B -h B ) = 0h ) |
16 |
15
|
ad2antlr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( B -h B ) = 0h ) |
17 |
16
|
oveq2d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A -h C ) +h ( B -h B ) ) = ( ( A -h C ) +h 0h ) ) |
18 |
|
hvsubcl |
|- ( ( A e. ~H /\ C e. ~H ) -> ( A -h C ) e. ~H ) |
19 |
|
ax-hvaddid |
|- ( ( A -h C ) e. ~H -> ( ( A -h C ) +h 0h ) = ( A -h C ) ) |
20 |
18 19
|
syl |
|- ( ( A e. ~H /\ C e. ~H ) -> ( ( A -h C ) +h 0h ) = ( A -h C ) ) |
21 |
20
|
adantlr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A -h C ) +h 0h ) = ( A -h C ) ) |
22 |
14 17 21
|
3eqtrd |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ C e. ~H ) -> ( ( A +h B ) -h ( C +h B ) ) = ( A -h C ) ) |
23 |
22
|
adantrr |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) -h ( C +h B ) ) = ( A -h C ) ) |
24 |
|
simpl |
|- ( ( C e. ~H /\ D e. ~H ) -> C e. ~H ) |
25 |
24
|
anim1i |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( C e. ~H /\ B e. ~H ) ) |
26 |
|
hvsub4 |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ ( C e. ~H /\ B e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( ( C -h C ) +h ( D -h B ) ) ) |
27 |
25 26
|
syldan |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C +h D ) -h ( C +h B ) ) = ( ( C -h C ) +h ( D -h B ) ) ) |
28 |
|
hvsubid |
|- ( C e. ~H -> ( C -h C ) = 0h ) |
29 |
28
|
ad2antrr |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( C -h C ) = 0h ) |
30 |
29
|
oveq1d |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C -h C ) +h ( D -h B ) ) = ( 0h +h ( D -h B ) ) ) |
31 |
|
hvsubcl |
|- ( ( D e. ~H /\ B e. ~H ) -> ( D -h B ) e. ~H ) |
32 |
|
hvaddid2 |
|- ( ( D -h B ) e. ~H -> ( 0h +h ( D -h B ) ) = ( D -h B ) ) |
33 |
31 32
|
syl |
|- ( ( D e. ~H /\ B e. ~H ) -> ( 0h +h ( D -h B ) ) = ( D -h B ) ) |
34 |
33
|
adantll |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( 0h +h ( D -h B ) ) = ( D -h B ) ) |
35 |
27 30 34
|
3eqtrd |
|- ( ( ( C e. ~H /\ D e. ~H ) /\ B e. ~H ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) ) |
36 |
35
|
ancoms |
|- ( ( B e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) ) |
37 |
36
|
adantll |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( C +h D ) -h ( C +h B ) ) = ( D -h B ) ) |
38 |
23 37
|
eqeq12d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A +h B ) -h ( C +h B ) ) = ( ( C +h D ) -h ( C +h B ) ) <-> ( A -h C ) = ( D -h B ) ) ) |
39 |
9 38
|
bitr3d |
|- ( ( ( A e. ~H /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A +h B ) = ( C +h D ) <-> ( A -h C ) = ( D -h B ) ) ) |