Step |
Hyp |
Ref |
Expression |
1 |
|
eigorthi.1 |
|- A e. ~H |
2 |
|
eigorthi.2 |
|- B e. ~H |
3 |
|
eigorthi.3 |
|- C e. CC |
4 |
|
eigorthi.4 |
|- D e. CC |
5 |
|
oveq2 |
|- ( ( T ` B ) = ( D .h B ) -> ( A .ih ( T ` B ) ) = ( A .ih ( D .h B ) ) ) |
6 |
|
his5 |
|- ( ( D e. CC /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( D .h B ) ) = ( ( * ` D ) x. ( A .ih B ) ) ) |
7 |
4 1 2 6
|
mp3an |
|- ( A .ih ( D .h B ) ) = ( ( * ` D ) x. ( A .ih B ) ) |
8 |
5 7
|
eqtrdi |
|- ( ( T ` B ) = ( D .h B ) -> ( A .ih ( T ` B ) ) = ( ( * ` D ) x. ( A .ih B ) ) ) |
9 |
|
oveq1 |
|- ( ( T ` A ) = ( C .h A ) -> ( ( T ` A ) .ih B ) = ( ( C .h A ) .ih B ) ) |
10 |
|
ax-his3 |
|- ( ( C e. CC /\ A e. ~H /\ B e. ~H ) -> ( ( C .h A ) .ih B ) = ( C x. ( A .ih B ) ) ) |
11 |
3 1 2 10
|
mp3an |
|- ( ( C .h A ) .ih B ) = ( C x. ( A .ih B ) ) |
12 |
9 11
|
eqtrdi |
|- ( ( T ` A ) = ( C .h A ) -> ( ( T ` A ) .ih B ) = ( C x. ( A .ih B ) ) ) |
13 |
8 12
|
eqeqan12rd |
|- ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) ) ) |
14 |
1 2
|
hicli |
|- ( A .ih B ) e. CC |
15 |
4
|
cjcli |
|- ( * ` D ) e. CC |
16 |
|
mulcan2 |
|- ( ( ( * ` D ) e. CC /\ C e. CC /\ ( ( A .ih B ) e. CC /\ ( A .ih B ) =/= 0 ) ) -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) <-> ( * ` D ) = C ) ) |
17 |
15 3 16
|
mp3an12 |
|- ( ( ( A .ih B ) e. CC /\ ( A .ih B ) =/= 0 ) -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) <-> ( * ` D ) = C ) ) |
18 |
14 17
|
mpan |
|- ( ( A .ih B ) =/= 0 -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) <-> ( * ` D ) = C ) ) |
19 |
|
eqcom |
|- ( ( * ` D ) = C <-> C = ( * ` D ) ) |
20 |
18 19
|
syl6bb |
|- ( ( A .ih B ) =/= 0 -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) <-> C = ( * ` D ) ) ) |
21 |
20
|
biimpcd |
|- ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) -> ( ( A .ih B ) =/= 0 -> C = ( * ` D ) ) ) |
22 |
21
|
necon1d |
|- ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) -> ( C =/= ( * ` D ) -> ( A .ih B ) = 0 ) ) |
23 |
22
|
com12 |
|- ( C =/= ( * ` D ) -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) -> ( A .ih B ) = 0 ) ) |
24 |
|
oveq2 |
|- ( ( A .ih B ) = 0 -> ( ( * ` D ) x. ( A .ih B ) ) = ( ( * ` D ) x. 0 ) ) |
25 |
|
oveq2 |
|- ( ( A .ih B ) = 0 -> ( C x. ( A .ih B ) ) = ( C x. 0 ) ) |
26 |
3
|
mul01i |
|- ( C x. 0 ) = 0 |
27 |
15
|
mul01i |
|- ( ( * ` D ) x. 0 ) = 0 |
28 |
26 27
|
eqtr4i |
|- ( C x. 0 ) = ( ( * ` D ) x. 0 ) |
29 |
25 28
|
eqtrdi |
|- ( ( A .ih B ) = 0 -> ( C x. ( A .ih B ) ) = ( ( * ` D ) x. 0 ) ) |
30 |
24 29
|
eqtr4d |
|- ( ( A .ih B ) = 0 -> ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) ) |
31 |
23 30
|
impbid1 |
|- ( C =/= ( * ` D ) -> ( ( ( * ` D ) x. ( A .ih B ) ) = ( C x. ( A .ih B ) ) <-> ( A .ih B ) = 0 ) ) |
32 |
13 31
|
sylan9bb |
|- ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) ) |