Metamath Proof Explorer

Theorem sn-negex12

Description: A combination of cnegex and cnegex2 , this proof takes cnre A = r +i x. s and shows that i x. -u s + -u r is both a left and right inverse. (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-negex12 
|- ( A e. CC -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 1 a1i 
 |-  ( y e. RR -> _i e. CC )
3 rernegcl 
 |-  ( y e. RR -> ( 0 -R y ) e. RR )
4 3 recnd 
 |-  ( y e. RR -> ( 0 -R y ) e. CC )
5 2 4 mulcld 
 |-  ( y e. RR -> ( _i x. ( 0 -R y ) ) e. CC )
6 5 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( 0 -R y ) ) e. CC )
7 rernegcl 
 |-  ( x e. RR -> ( 0 -R x ) e. RR )
8 7 recnd 
 |-  ( x e. RR -> ( 0 -R x ) e. CC )
9 8 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 -R x ) e. CC )
10 6 9 addcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) e. CC )
11 10 adantl 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) e. CC )
12 eqeq1 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) <-> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
13 12 adantl 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) -> ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) <-> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
14 eqidd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) )
15 11 13 14 rspcedvd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) )
16 15 ralrimivva 
 |-  ( A e. CC -> A. x e. RR A. y e. RR E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) )
17 cnre 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
18 16 17 r19.29d2r 
 |-  ( A e. CC -> E. x e. RR E. y e. RR ( E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) /\ A = ( x + ( _i x. y ) ) ) )
19 oveq1 
 |-  ( A = ( x + ( _i x. y ) ) -> ( A + ( _i x. ( 0 -R y ) ) ) = ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) )
20 19 adantl 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( A + ( _i x. ( 0 -R y ) ) ) = ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) )
21 recn 
 |-  ( x e. RR -> x e. CC )
22 21 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. CC )
23 1 a1i 
 |-  ( ( x e. RR /\ y e. RR ) -> _i e. CC )
24 recn 
 |-  ( y e. RR -> y e. CC )
25 24 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. CC )
26 23 25 mulcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) e. CC )
27 22 26 6 addassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) = ( x + ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) ) )
28 renegid 
 |-  ( y e. RR -> ( y + ( 0 -R y ) ) = 0 )
29 28 oveq2d 
 |-  ( y e. RR -> ( _i x. ( y + ( 0 -R y ) ) ) = ( _i x. 0 ) )
30 2 24 4 adddid 
 |-  ( y e. RR -> ( _i x. ( y + ( 0 -R y ) ) ) = ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) )
31 sn-it0e0 
 |-  ( _i x. 0 ) = 0
32 31 a1i 
 |-  ( y e. RR -> ( _i x. 0 ) = 0 )
33 29 30 32 3eqtr3d 
 |-  ( y e. RR -> ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) = 0 )
34 33 oveq2d 
 |-  ( y e. RR -> ( x + ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) ) = ( x + 0 ) )
35 34 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) ) = ( x + 0 ) )
36 readdid1 
 |-  ( x e. RR -> ( x + 0 ) = x )
37 36 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + 0 ) = x )
38 27 35 37 3eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) = x )
39 38 ad2antlr 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) = x )
40 20 39 eqtrd 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( A + ( _i x. ( 0 -R y ) ) ) = x )
41 40 oveq1d 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( A + ( _i x. ( 0 -R y ) ) ) + ( 0 -R x ) ) = ( x + ( 0 -R x ) ) )
42 simpll 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> A e. CC )
43 6 ad2antlr 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( _i x. ( 0 -R y ) ) e. CC )
44 9 ad2antlr 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( 0 -R x ) e. CC )
45 42 43 44 addassd 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( A + ( _i x. ( 0 -R y ) ) ) + ( 0 -R x ) ) = ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
46 renegid 
 |-  ( x e. RR -> ( x + ( 0 -R x ) ) = 0 )
47 46 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( 0 -R x ) ) = 0 )
48 47 ad2antlr 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( x + ( 0 -R x ) ) = 0 )
49 41 45 48 3eqtr3d 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 )
50 oveq2 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) = ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) )
51 22 26 addcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) e. CC )
52 6 9 51 addassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = ( ( _i x. ( 0 -R y ) ) + ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) ) )
53 9 22 26 addassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) = ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) )
54 53 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) ) = ( ( _i x. ( 0 -R y ) ) + ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) ) )
55 renegid2 
 |-  ( x e. RR -> ( ( 0 -R x ) + x ) = 0 )
56 55 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 0 -R x ) + x ) = 0 )
57 56 oveq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) = ( 0 + ( _i x. y ) ) )
58 sn-addid2 
 |-  ( ( _i x. y ) e. CC -> ( 0 + ( _i x. y ) ) = ( _i x. y ) )
59 26 58 syl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 + ( _i x. y ) ) = ( _i x. y ) )
60 57 59 eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) = ( _i x. y ) )
61 60 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) ) = ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) )
62 4 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 -R y ) e. CC )
63 23 62 25 adddid 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( ( 0 -R y ) + y ) ) = ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) )
64 renegid2 
 |-  ( y e. RR -> ( ( 0 -R y ) + y ) = 0 )
65 64 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 0 -R y ) + y ) = 0 )
66 65 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( ( 0 -R y ) + y ) ) = ( _i x. 0 ) )
67 66 31 eqtrdi 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( ( 0 -R y ) + y ) ) = 0 )
68 61 63 67 3eqtr2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) ) = 0 )
69 52 54 68 3eqtr2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 )
70 69 adantl 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 )
71 50 70 sylan9eqr 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) = 0 )
72 49 71 jca 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 /\ ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) = 0 ) )
73 oveq2 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( A + b ) = ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
74 73 eqeq1d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( A + b ) = 0 <-> ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 ) )
75 oveq1 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( b + A ) = ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) )
76 75 eqeq1d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( b + A ) = 0 <-> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) = 0 ) )
77 74 76 anbi12d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( ( A + b ) = 0 /\ ( b + A ) = 0 ) <-> ( ( A + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 /\ ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + A ) = 0 ) ) )
78 72 77 syl5ibrcom 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
79 78 reximdv 
 |-  ( ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) /\ A = ( x + ( _i x. y ) ) ) -> ( E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
80 79 expimpd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( ( A = ( x + ( _i x. y ) ) /\ E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
81 80 ancomsd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( ( E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) /\ A = ( x + ( _i x. y ) ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
82 81 rexlimdvva 
 |-  ( A e. CC -> ( E. x e. RR E. y e. RR ( E. b e. CC b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) /\ A = ( x + ( _i x. y ) ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
83 18 82 mpd 
 |-  ( A e. CC -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) )