Metamath Proof Explorer

Theorem angcan

Description: Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion angcan 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) F ( C x. B ) ) = ( A F B ) )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
3 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
4 simp3l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
5 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> A =/= 0 )
6 simp3r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 )
7 2 3 4 5 6 divcan5d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / ( C x. A ) ) = ( B / A ) )
8 7 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( log ` ( ( C x. B ) / ( C x. A ) ) ) = ( log ` ( B / A ) ) )
9 8 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( Im ` ( log ` ( ( C x. B ) / ( C x. A ) ) ) ) = ( Im ` ( log ` ( B / A ) ) ) )
10 4 3 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) e. CC )
11 4 3 6 5 mulne0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. A ) =/= 0 )
12 4 2 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. B ) e. CC )
13 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> B =/= 0 )
14 4 2 6 13 mulne0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. B ) =/= 0 )
15 1 angval 
 |-  ( ( ( ( C x. A ) e. CC /\ ( C x. A ) =/= 0 ) /\ ( ( C x. B ) e. CC /\ ( C x. B ) =/= 0 ) ) -> ( ( C x. A ) F ( C x. B ) ) = ( Im ` ( log ` ( ( C x. B ) / ( C x. A ) ) ) ) )
16 10 11 12 14 15 syl22anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) F ( C x. B ) ) = ( Im ` ( log ` ( ( C x. B ) / ( C x. A ) ) ) ) )
17 1 angval 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A F B ) = ( Im ` ( log ` ( B / A ) ) ) )
18 17 3adant3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( A F B ) = ( Im ` ( log ` ( B / A ) ) ) )
19 9 16 18 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. A ) F ( C x. B ) ) = ( A F B ) )