Metamath Proof Explorer

Theorem imadd

Description: Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

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

Proof

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