Step |
Hyp |
Ref |
Expression |
1 |
|
hisubcom.1 |
|- A e. ~H |
2 |
|
hisubcom.2 |
|- B e. ~H |
3 |
|
hisubcom.3 |
|- C e. ~H |
4 |
|
hisubcom.4 |
|- D e. ~H |
5 |
2 1
|
hvnegdii |
|- ( -u 1 .h ( B -h A ) ) = ( A -h B ) |
6 |
4 3
|
hvnegdii |
|- ( -u 1 .h ( D -h C ) ) = ( C -h D ) |
7 |
5 6
|
oveq12i |
|- ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( A -h B ) .ih ( C -h D ) ) |
8 |
|
neg1cn |
|- -u 1 e. CC |
9 |
2 1
|
hvsubcli |
|- ( B -h A ) e. ~H |
10 |
4 3
|
hvsubcli |
|- ( D -h C ) e. ~H |
11 |
8 8 9 10
|
his35i |
|- ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( -u 1 x. ( * ` -u 1 ) ) x. ( ( B -h A ) .ih ( D -h C ) ) ) |
12 |
|
neg1rr |
|- -u 1 e. RR |
13 |
|
cjre |
|- ( -u 1 e. RR -> ( * ` -u 1 ) = -u 1 ) |
14 |
12 13
|
ax-mp |
|- ( * ` -u 1 ) = -u 1 |
15 |
14
|
oveq2i |
|- ( -u 1 x. ( * ` -u 1 ) ) = ( -u 1 x. -u 1 ) |
16 |
|
ax-1cn |
|- 1 e. CC |
17 |
16 16
|
mul2negi |
|- ( -u 1 x. -u 1 ) = ( 1 x. 1 ) |
18 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
19 |
15 17 18
|
3eqtri |
|- ( -u 1 x. ( * ` -u 1 ) ) = 1 |
20 |
19
|
oveq1i |
|- ( ( -u 1 x. ( * ` -u 1 ) ) x. ( ( B -h A ) .ih ( D -h C ) ) ) = ( 1 x. ( ( B -h A ) .ih ( D -h C ) ) ) |
21 |
9 10
|
hicli |
|- ( ( B -h A ) .ih ( D -h C ) ) e. CC |
22 |
21
|
mulid2i |
|- ( 1 x. ( ( B -h A ) .ih ( D -h C ) ) ) = ( ( B -h A ) .ih ( D -h C ) ) |
23 |
11 20 22
|
3eqtri |
|- ( ( -u 1 .h ( B -h A ) ) .ih ( -u 1 .h ( D -h C ) ) ) = ( ( B -h A ) .ih ( D -h C ) ) |
24 |
7 23
|
eqtr3i |
|- ( ( A -h B ) .ih ( C -h D ) ) = ( ( B -h A ) .ih ( D -h C ) ) |