let a, b be Element of COMPLEX ; :: thesis: ( a <> 0 & b <> 0 implies ( cos (angle a,b) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle a,b) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) ) )
assume that
A1: a <> 0 and
A2: b <> 0 ; :: thesis: ( cos (angle a,b) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle a,b) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) )
A3: ( |.a.| <> 0 & |.b.| <> 0 ) by A1, A2, COMPLEX1:131;
set ra = Rotate a,(- (Arg a));
set rb = Rotate b,(- (Arg a));
set r = - (Arg a);
set mabi = (|.a.| * |.b.|) " ;
A4: ( |.a.| >= 0 & |.b.| >= 0 ) by COMPLEX1:132;
angle a,b = angle (Rotate a,(- (Arg a))),(Rotate b,(- (Arg a))) by A1, A2, Th79;
then A5: angle a,b = angle (|.a.| * ((|.a.| * |.b.|) " )),((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )) by A3, A4, Th77, SIN_COS:34
.= Arg ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )) by A4, Th75 ;
A6: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i> ) by Th19;
then Re a = |.a.| * (cos (Arg a)) by COMPLEX1:28;
then A7: cos (Arg a) = (Re a) / |.a.| by A1, COMPLEX1:131, XCMPLX_1:90;
Im a = |.a.| * (sin (Arg a)) by A6, COMPLEX1:28;
then A8: sin (Arg a) = (Im a) / |.a.| by A1, COMPLEX1:131, XCMPLX_1:90;
A9: a .|. b = (((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i> ) by Th42;
then A10: Re (a .|. b) = ((Re a) * (Re b)) + ((Im a) * (Im b)) by COMPLEX1:28;
Re (Rotate b,(- (Arg a))) = ((Re b) * (cos (- (Arg a)))) - ((Im b) * (sin (- (Arg a)))) by Th70;
then A11: Re (Rotate b,(- (Arg a))) = ((Re b) * (cos (- (Arg a)))) - ((Im b) * (- (sin (Arg a)))) by SIN_COS:34
.= ((Re b) * ((Re a) / |.a.|)) + ((Im b) * ((Im a) / |.a.|)) by A7, A8, SIN_COS:34
.= (Re (a .|. b)) / |.a.| by A10 ;
A12: (Im (Rotate b,(- (Arg a)))) ^2 >= 0 by XREAL_1:65;
Im (Rotate b,(- (Arg a))) = ((Re b) * (sin (- (Arg a)))) + ((Im b) * (cos (- (Arg a)))) by Th70;
then A13: Im (Rotate b,(- (Arg a))) = ((Re b) * (- (sin (Arg a)))) + ((Im b) * (cos (- (Arg a)))) by SIN_COS:34
.= ((- (Re b)) * ((Im a) / |.a.|)) + ((Im b) * ((Re a) / |.a.|)) by A7, A8, SIN_COS:34
.= - ((- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) / |.a.|)
.= - ((Im (a .|. b)) / |.a.|) by A9, COMPLEX1:28 ;
set IT = (Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " );
set mab = |.a.| * |.b.|;
A14: ( ((|.a.| * |.b.|) " ) ^2 >= 0 & (Re (Rotate b,(- (Arg a)))) ^2 >= 0 ) by XREAL_1:65;
(|.a.| * |.b.|) " = ((|.a.| * |.b.|) " ) + (0 * <i> ) ;
then A15: ( Re ((|.a.| * |.b.|) " ) = (|.a.| * |.b.|) " & Im ((|.a.| * |.b.|) " ) = 0 ) by COMPLEX1:28;
then A16: Re ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )) = ((Re (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) - ((Im (Rotate b,(- (Arg a)))) * 0 ) by COMPLEX1:24
.= (Re (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " ) ;
A17: Im ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )) = ((Re (Rotate b,(- (Arg a)))) * 0 ) + ((Im (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) by A15, COMPLEX1:24
.= (Im (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " ) ;
then A18: |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| = sqrt ((((Re (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) ^2 ) + (((Im (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) ^2 )) by A16, COMPLEX1:def 16
.= sqrt ((((|.a.| * |.b.|) " ) ^2 ) * (((Re (Rotate b,(- (Arg a)))) ^2 ) + ((Im (Rotate b,(- (Arg a)))) ^2 )))
.= (sqrt (((|.a.| * |.b.|) " ) ^2 )) * (sqrt (((Re (Rotate b,(- (Arg a)))) ^2 ) + ((Im (Rotate b,(- (Arg a)))) ^2 ))) by A14, A12, SQUARE_1:97
.= ((|.a.| * |.b.|) " ) * (sqrt (((Re (Rotate b,(- (Arg a)))) ^2 ) + ((Im (Rotate b,(- (Arg a)))) ^2 ))) by A4, SQUARE_1:89
.= ((|.a.| * |.b.|) " ) * |.(Rotate b,(- (Arg a))).| by COMPLEX1:def 16
.= ((|.a.| * |.b.|) " ) * |.b.| by Th67 ;
A19: (Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " ) = (|.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| * (cos (Arg ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " ))))) + ((|.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| * (sin (Arg ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " ))))) * <i> ) by Th19;
then |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| * (cos (Arg ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )))) = (Re (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " ) by A16, COMPLEX1:28;
hence cos (angle a,b) = ((Re (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) / |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| by A3, A5, A18, XCMPLX_1:90
.= (Re (Rotate b,(- (Arg a)))) * (((|.a.| * |.b.|) " ) / |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).|)
.= ((Re (a .|. b)) / |.a.|) * ((((|.a.| * |.b.|) " ) / ((|.a.| * |.b.|) " )) / |.b.|) by A11, A18, XCMPLX_1:79
.= ((Re (a .|. b)) / |.a.|) * (1 / |.b.|) by A3, XCMPLX_1:60
.= ((Re (a .|. b)) * 1) / (|.a.| * |.b.|) by XCMPLX_1:77
.= (Re (a .|. b)) / (|.a.| * |.b.|) ;
:: thesis: sin (angle a,b) = - ((Im (a .|. b)) / (|.a.| * |.b.|))
|.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| * (sin (Arg ((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )))) = (Im (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " ) by A19, A17, COMPLEX1:28;
hence sin (angle a,b) = ((Im (Rotate b,(- (Arg a)))) * ((|.a.| * |.b.|) " )) / |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).| by A3, A5, A18, XCMPLX_1:90
.= (Im (Rotate b,(- (Arg a)))) * (((|.a.| * |.b.|) " ) / |.((Rotate b,(- (Arg a))) * ((|.a.| * |.b.|) " )).|)
.= (- ((Im (a .|. b)) / |.a.|)) * ((((|.a.| * |.b.|) " ) / ((|.a.| * |.b.|) " )) / |.b.|) by A13, A18, XCMPLX_1:79
.= ((- (Im (a .|. b))) / |.a.|) * (1 / |.b.|) by A3, XCMPLX_1:60
.= ((- (Im (a .|. b))) * 1) / (|.a.| * |.b.|) by XCMPLX_1:77
.= - ((Im (a .|. b)) / (|.a.| * |.b.|)) ;
:: thesis: verum