Step |
Hyp |
Ref |
Expression |
1 |
|
his5 |
|- ( ( B e. CC /\ C e. ~H /\ D e. ~H ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) ) |
2 |
1
|
3expb |
|- ( ( B e. CC /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) ) |
3 |
2
|
adantll |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) ) |
4 |
3
|
oveq2d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A x. ( C .ih ( B .h D ) ) ) = ( A x. ( ( * ` B ) x. ( C .ih D ) ) ) ) |
5 |
|
simpll |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> A e. CC ) |
6 |
|
simprl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> C e. ~H ) |
7 |
|
hvmulcl |
|- ( ( B e. CC /\ D e. ~H ) -> ( B .h D ) e. ~H ) |
8 |
7
|
ad2ant2l |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( B .h D ) e. ~H ) |
9 |
|
ax-his3 |
|- ( ( A e. CC /\ C e. ~H /\ ( B .h D ) e. ~H ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( A x. ( C .ih ( B .h D ) ) ) ) |
10 |
5 6 8 9
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( A x. ( C .ih ( B .h D ) ) ) ) |
11 |
|
cjcl |
|- ( B e. CC -> ( * ` B ) e. CC ) |
12 |
11
|
ad2antlr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( * ` B ) e. CC ) |
13 |
|
hicl |
|- ( ( C e. ~H /\ D e. ~H ) -> ( C .ih D ) e. CC ) |
14 |
13
|
adantl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih D ) e. CC ) |
15 |
5 12 14
|
mulassd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A x. ( * ` B ) ) x. ( C .ih D ) ) = ( A x. ( ( * ` B ) x. ( C .ih D ) ) ) ) |
16 |
4 10 15
|
3eqtr4d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( ( A x. ( * ` B ) ) x. ( C .ih D ) ) ) |