Metamath Proof Explorer

Theorem cjadd

Description: Complex conjugate distributes over addition. Proposition 10-3.4(a) of Gleason p. 133. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjadd 
|- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )

Proof

Step Hyp Ref Expression
1 readd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
2 imadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
3 2 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` ( A + B ) ) ) = ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) )
4 ax-icn 
 |-  _i e. CC
5 4 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i e. CC )
6 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
7 6 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. RR )
8 7 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. CC )
9 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
10 9 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. RR )
11 10 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. CC )
12 5 8 11 adddid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( Im ` A ) + ( Im ` B ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) )
13 3 12 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` ( A + B ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) )
14 1 13 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A + B ) ) - ( _i x. ( Im ` ( A + B ) ) ) ) = ( ( ( Re ` A ) + ( Re ` B ) ) - ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) ) )
15 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
16 15 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. RR )
17 16 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. CC )
18 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
19 18 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. RR )
20 19 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. CC )
21 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
22 4 8 21 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
23 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
24 4 11 23 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
25 17 20 22 24 addsub4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( Re ` B ) ) - ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) + ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) )
26 14 25 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A + B ) ) - ( _i x. ( Im ` ( A + B ) ) ) ) = ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) + ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) )
27 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
28 remim 
 |-  ( ( A + B ) e. CC -> ( * ` ( A + B ) ) = ( ( Re ` ( A + B ) ) - ( _i x. ( Im ` ( A + B ) ) ) ) )
29 27 28 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + B ) ) = ( ( Re ` ( A + B ) ) - ( _i x. ( Im ` ( A + B ) ) ) ) )
30 remim 
 |-  ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
31 remim 
 |-  ( B e. CC -> ( * ` B ) = ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) )
32 30 31 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) + ( * ` B ) ) = ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) + ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) )
33 26 29 32 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )