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) (Proof shortened by SN, 4-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
2 oveq2 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( x + ( _i x. y ) ) + b ) = ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
3 2 eqeq1d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( ( x + ( _i x. y ) ) + b ) = 0 <-> ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 ) )
4 oveq1 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( b + ( x + ( _i x. y ) ) ) = ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) )
5 4 eqeq1d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( b + ( x + ( _i x. y ) ) ) = 0 <-> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 ) )
6 3 5 anbi12d 
 |-  ( b = ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) -> ( ( ( ( x + ( _i x. y ) ) + b ) = 0 /\ ( b + ( x + ( _i x. y ) ) ) = 0 ) <-> ( ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 /\ ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 ) ) )
7 ax-icn 
 |-  _i e. CC
8 7 a1i 
 |-  ( y e. RR -> _i e. CC )
9 rernegcl 
 |-  ( y e. RR -> ( 0 -R y ) e. RR )
10 9 recnd 
 |-  ( y e. RR -> ( 0 -R y ) e. CC )
11 8 10 mulcld 
 |-  ( y e. RR -> ( _i x. ( 0 -R y ) ) e. CC )
12 11 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( 0 -R y ) ) e. CC )
13 rernegcl 
 |-  ( x e. RR -> ( 0 -R x ) e. RR )
14 13 recnd 
 |-  ( x e. RR -> ( 0 -R x ) e. CC )
15 14 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 -R x ) e. CC )
16 12 15 addcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) e. CC )
17 recn 
 |-  ( x e. RR -> x e. CC )
18 17 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. CC )
19 recn 
 |-  ( y e. RR -> y e. CC )
20 8 19 mulcld 
 |-  ( y e. RR -> ( _i x. y ) e. CC )
21 20 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) e. CC )
22 18 21 12 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 ) ) ) ) )
23 8 19 10 adddid 
 |-  ( y e. RR -> ( _i x. ( y + ( 0 -R y ) ) ) = ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) )
24 renegid 
 |-  ( y e. RR -> ( y + ( 0 -R y ) ) = 0 )
25 24 oveq2d 
 |-  ( y e. RR -> ( _i x. ( y + ( 0 -R y ) ) ) = ( _i x. 0 ) )
26 sn-it0e0 
 |-  ( _i x. 0 ) = 0
27 25 26 eqtrdi 
 |-  ( y e. RR -> ( _i x. ( y + ( 0 -R y ) ) ) = 0 )
28 23 27 eqtr3d 
 |-  ( y e. RR -> ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) = 0 )
29 28 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) = 0 )
30 29 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( ( _i x. y ) + ( _i x. ( 0 -R y ) ) ) ) = ( x + 0 ) )
31 readdrid 
 |-  ( x e. RR -> ( x + 0 ) = x )
32 31 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + 0 ) = x )
33 22 30 32 3eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) = x )
34 33 oveq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) + ( 0 -R x ) ) = ( x + ( 0 -R x ) ) )
35 18 21 addcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( _i x. y ) ) e. CC )
36 35 12 15 addassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( _i x. y ) ) + ( _i x. ( 0 -R y ) ) ) + ( 0 -R x ) ) = ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) )
37 renegid 
 |-  ( x e. RR -> ( x + ( 0 -R x ) ) = 0 )
38 37 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + ( 0 -R x ) ) = 0 )
39 34 36 38 3eqtr3d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 )
40 12 15 35 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 ) ) ) ) )
41 renegid2 
 |-  ( x e. RR -> ( ( 0 -R x ) + x ) = 0 )
42 41 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 0 -R x ) + x ) = 0 )
43 42 oveq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) = ( 0 + ( _i x. y ) ) )
44 15 18 21 addassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( 0 -R x ) + x ) + ( _i x. y ) ) = ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) )
45 sn-addlid 
 |-  ( ( _i x. y ) e. CC -> ( 0 + ( _i x. y ) ) = ( _i x. y ) )
46 21 45 syl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 + ( _i x. y ) ) = ( _i x. y ) )
47 43 44 46 3eqtr3rd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) = ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) )
48 47 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) = ( ( _i x. ( 0 -R y ) ) + ( ( 0 -R x ) + ( x + ( _i x. y ) ) ) ) )
49 8 10 19 adddid 
 |-  ( y e. RR -> ( _i x. ( ( 0 -R y ) + y ) ) = ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) )
50 renegid2 
 |-  ( y e. RR -> ( ( 0 -R y ) + y ) = 0 )
51 50 oveq2d 
 |-  ( y e. RR -> ( _i x. ( ( 0 -R y ) + y ) ) = ( _i x. 0 ) )
52 51 26 eqtrdi 
 |-  ( y e. RR -> ( _i x. ( ( 0 -R y ) + y ) ) = 0 )
53 49 52 eqtr3d 
 |-  ( y e. RR -> ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) = 0 )
54 53 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. ( 0 -R y ) ) + ( _i x. y ) ) = 0 )
55 40 48 54 3eqtr2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 )
56 39 55 jca 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( x + ( _i x. y ) ) + ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) ) = 0 /\ ( ( ( _i x. ( 0 -R y ) ) + ( 0 -R x ) ) + ( x + ( _i x. y ) ) ) = 0 ) )
57 6 16 56 rspcedvdw 
 |-  ( ( x e. RR /\ y e. RR ) -> E. b e. CC ( ( ( x + ( _i x. y ) ) + b ) = 0 /\ ( b + ( x + ( _i x. y ) ) ) = 0 ) )
58 57 adantl 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> E. b e. CC ( ( ( x + ( _i x. y ) ) + b ) = 0 /\ ( b + ( x + ( _i x. y ) ) ) = 0 ) )
59 oveq1 
 |-  ( A = ( x + ( _i x. y ) ) -> ( A + b ) = ( ( x + ( _i x. y ) ) + b ) )
60 59 eqeq1d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( A + b ) = 0 <-> ( ( x + ( _i x. y ) ) + b ) = 0 ) )
61 oveq2 
 |-  ( A = ( x + ( _i x. y ) ) -> ( b + A ) = ( b + ( x + ( _i x. y ) ) ) )
62 61 eqeq1d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( b + A ) = 0 <-> ( b + ( x + ( _i x. y ) ) ) = 0 ) )
63 60 62 anbi12d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( ( A + b ) = 0 /\ ( b + A ) = 0 ) <-> ( ( ( x + ( _i x. y ) ) + b ) = 0 /\ ( b + ( x + ( _i x. y ) ) ) = 0 ) ) )
64 63 rexbidv 
 |-  ( A = ( x + ( _i x. y ) ) -> ( E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) <-> E. b e. CC ( ( ( x + ( _i x. y ) ) + b ) = 0 /\ ( b + ( x + ( _i x. y ) ) ) = 0 ) ) )
65 58 64 syl5ibrcom 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) ) -> ( A = ( x + ( _i x. y ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
66 65 rexlimdvva 
 |-  ( A e. CC -> ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) ) )
67 1 66 mpd 
 |-  ( A e. CC -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) )