Metamath Proof Explorer


Theorem recj

Description: Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion recj ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ( โˆ— โ€˜ ๐ด ) ) = ( โ„œ โ€˜ ๐ด ) )

Proof

Step Hyp Ref Expression
1 recl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ๐ด ) โˆˆ โ„ )
2 1 recnd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ๐ด ) โˆˆ โ„‚ )
3 ax-icn โŠข i โˆˆ โ„‚
4 imcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„ )
5 4 recnd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„‚ )
6 mulcl โŠข ( ( i โˆˆ โ„‚ โˆง ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„‚ ) โ†’ ( i ยท ( โ„‘ โ€˜ ๐ด ) ) โˆˆ โ„‚ )
7 3 5 6 sylancr โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( i ยท ( โ„‘ โ€˜ ๐ด ) ) โˆˆ โ„‚ )
8 2 7 negsubd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( โ„œ โ€˜ ๐ด ) + - ( i ยท ( โ„‘ โ€˜ ๐ด ) ) ) = ( ( โ„œ โ€˜ ๐ด ) โˆ’ ( i ยท ( โ„‘ โ€˜ ๐ด ) ) ) )
9 mulneg2 โŠข ( ( i โˆˆ โ„‚ โˆง ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„‚ ) โ†’ ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) = - ( i ยท ( โ„‘ โ€˜ ๐ด ) ) )
10 3 5 9 sylancr โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) = - ( i ยท ( โ„‘ โ€˜ ๐ด ) ) )
11 10 oveq2d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( โ„œ โ€˜ ๐ด ) + ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) ) = ( ( โ„œ โ€˜ ๐ด ) + - ( i ยท ( โ„‘ โ€˜ ๐ด ) ) ) )
12 remim โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โˆ— โ€˜ ๐ด ) = ( ( โ„œ โ€˜ ๐ด ) โˆ’ ( i ยท ( โ„‘ โ€˜ ๐ด ) ) ) )
13 8 11 12 3eqtr4rd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โˆ— โ€˜ ๐ด ) = ( ( โ„œ โ€˜ ๐ด ) + ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) ) )
14 13 fveq2d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ( โˆ— โ€˜ ๐ด ) ) = ( โ„œ โ€˜ ( ( โ„œ โ€˜ ๐ด ) + ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) ) ) )
15 4 renegcld โŠข ( ๐ด โˆˆ โ„‚ โ†’ - ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„ )
16 crre โŠข ( ( ( โ„œ โ€˜ ๐ด ) โˆˆ โ„ โˆง - ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„ ) โ†’ ( โ„œ โ€˜ ( ( โ„œ โ€˜ ๐ด ) + ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) ) ) = ( โ„œ โ€˜ ๐ด ) )
17 1 15 16 syl2anc โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ( ( โ„œ โ€˜ ๐ด ) + ( i ยท - ( โ„‘ โ€˜ ๐ด ) ) ) ) = ( โ„œ โ€˜ ๐ด ) )
18 14 17 eqtrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โ„œ โ€˜ ( โˆ— โ€˜ ๐ด ) ) = ( โ„œ โ€˜ ๐ด ) )