Metamath Proof Explorer


Theorem cjth

Description: The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion cjth ( ๐ด โˆˆ โ„‚ โ†’ ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) )

Proof

Step Hyp Ref Expression
1 cju โŠข ( ๐ด โˆˆ โ„‚ โ†’ โˆƒ! ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) )
2 riotasbc โŠข ( โˆƒ! ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) โ†’ [ ( โ„ฉ ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) )
3 1 2 syl โŠข ( ๐ด โˆˆ โ„‚ โ†’ [ ( โ„ฉ ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) )
4 cjval โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โˆ— โ€˜ ๐ด ) = ( โ„ฉ ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) ) )
5 4 sbceq1d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( [ ( โˆ— โ€˜ ๐ด ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) โ†” [ ( โ„ฉ ๐‘ฅ โˆˆ โ„‚ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) ) )
6 3 5 mpbird โŠข ( ๐ด โˆˆ โ„‚ โ†’ [ ( โˆ— โ€˜ ๐ด ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) )
7 fvex โŠข ( โˆ— โ€˜ ๐ด ) โˆˆ V
8 oveq2 โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( ๐ด + ๐‘ฅ ) = ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) )
9 8 eleq1d โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โ†” ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ ) )
10 oveq2 โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( ๐ด โˆ’ ๐‘ฅ ) = ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) )
11 10 oveq2d โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) = ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) )
12 11 eleq1d โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ โ†” ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) )
13 9 12 anbi12d โŠข ( ๐‘ฅ = ( โˆ— โ€˜ ๐ด ) โ†’ ( ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) โ†” ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) ) )
14 7 13 sbcie โŠข ( [ ( โˆ— โ€˜ ๐ด ) / ๐‘ฅ ] ( ( ๐ด + ๐‘ฅ ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ๐‘ฅ ) ) โˆˆ โ„ ) โ†” ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) )
15 6 14 sylib โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( ๐ด + ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( i ยท ( ๐ด โˆ’ ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ ) )