Theorem cnvtr 10609

Description: Converse of a translation.

Assertion

Ref	Expression
cnvtr	|- (A e. RR -> `'(x e. RR |-> (x + A)) = (x e. RR |-> (x - A)))

Distinct variable group:   x,A

Proof of Theorem cnvtr

Step	Hyp	Ref	Expression
1		f1ocnvfv 3886	. . . . . 6 |- (((x e. RR |-> (x + A)):RR-1-1-onto->RR /\ (x - A) e. RR) -> (((x e. RR |-> (x + A))` (x - A)) = x -> (`'(x e. RR |-> (x + A))` x) = (x - A)))
2		ax-17 973	. . . . . . . . . . 11 |- ((x e. RR /\ y = (x + A)) -> A.u(x e. RR /\ y = (x + A)))
3		ax-17 973	. . . . . . . . . . 11 |- ((x e. RR /\ y = (x + A)) -> A.v(x e. RR /\ y = (x + A)))
4		ax-17 973	. . . . . . . . . . 11 |- ((u e. RR /\ v = (u + A)) -> A.x(u e. RR /\ v = (u + A)))
5		ax-17 973	. . . . . . . . . . 11 |- ((u e. RR /\ v = (u + A)) -> A.y(u e. RR /\ v = (u + A)))
6		eleq1 1537	. . . . . . . . . . . . 13 |- (x = u -> (x e. RR <-> u e. RR))
7	6	adantr 391	. . . . . . . . . . . 12 |- ((x = u /\ y = v) -> (x e. RR <-> u e. RR))
8		eqeq1 1484	. . . . . . . . . . . . 13 |- (y = v -> (y = (x + A) <-> v = (x + A)))
9		opreq1 3974	. . . . . . . . . . . . . 14 |- (x = u -> (x + A) = (u + A))
10	9	eqeq2d 1489	. . . . . . . . . . . . 13 |- (x = u -> (v = (x + A) <-> v = (u + A)))
11	8, 10	sylan9bbr 543	. . . . . . . . . . . 12 |- ((x = u /\ y = v) -> (y = (x + A) <-> v = (u + A)))
12	7, 11	anbi12d 630	. . . . . . . . . . 11 |- ((x = u /\ y = v) -> ((x e. RR /\ y = (x + A)) <-> (u e. RR /\ v = (u + A))))
13	2, 3, 4, 5, 12	cbvopab 2677	. . . . . . . . . 10 |- {<.x, y>. | (x e. RR /\ y = (x + A))} = {<.u, v>. | (u e. RR /\ v = (u + A))}
14		df-mpt 4079	. . . . . . . . . 10 |- (x e. RR |-> (x + A)) = {<.x, y>. | (x e. RR /\ y = (x + A))}
15		df-mpt 4079	. . . . . . . . . 10 |- (u e. RR |-> (u + A)) = {<.u, v>. | (u e. RR /\ v = (u + A))}
16	13, 14, 15	3eqtr4 1508	. . . . . . . . 9 |- (x e. RR |-> (x + A)) = (u e. RR |-> (u + A))
17	16	trnij 10608	. . . . . . . 8 |- (A e. RR -> (x e. RR |-> (x + A)):RR-1-1-onto->RR)
18	17	adantr 391	. . . . . . 7 |- ((A e. RR /\ x e. RR) -> (x e. RR |-> (x + A)):RR-1-1-onto->RR)
19		resubclt 5450	. . . . . . . 8 |- ((x e. RR /\ A e. RR) -> (x - A) e. RR)
20	19	ancoms 438	. . . . . . 7 |- ((A e. RR /\ x e. RR) -> (x - A) e. RR)
21	18, 20	jca 288	. . . . . 6 |- ((A e. RR /\ x e. RR) -> ((x e. RR |-> (x + A)):RR-1-1-onto->RR /\ (x - A) e. RR))
22		eleq1 1537	. . . . . . . . . . . . 13 |- (y = x -> (y e. RR <-> x e. RR))
23	22	adantr 391	. . . . . . . . . . . 12 |- ((y = x /\ z = w) -> (y e. RR <-> x e. RR))
24		eqeq1 1484	. . . . . . . . . . . . 13 |- (z = w -> (z = (y + A) <-> w = (y + A)))
25		opreq1 3974	. . . . . . . . . . . . . 14 |- (y = x -> (y + A) = (x + A))
26	25	eqeq2d 1489	. . . . . . . . . . . . 13 |- (y = x -> (w = (y + A) <-> w = (x + A)))
27	24, 26	sylan9bbr 543	. . . . . . . . . . . 12 |- ((y = x /\ z = w) -> (z = (y + A) <-> w = (x + A)))
28	23, 27	anbi12d 630	. . . . . . . . . . 11 |- ((y = x /\ z = w) -> ((y e. RR /\ z = (y + A)) <-> (x e. RR /\ w = (x + A))))
29	28	cbvopabv 2678	. . . . . . . . . 10 |- {<.y, z>. | (y e. RR /\ z = (y + A))} = {<.x, w>. | (x e. RR /\ w = (x + A))}
30		df-mpt 4079	. . . . . . . . . 10 |- (y e. RR |-> (y + A)) = {<.y, z>. | (y e. RR /\ z = (y + A))}
31		df-mpt 4079	. . . . . . . . . 10 |- (x e. RR |-> (x + A)) = {<.x, w>. | (x e. RR /\ w = (x + A))}
32	29, 30, 31	3eqtr4r 1509	. . . . . . . . 9 |- (x e. RR |-> (x + A)) = (y e. RR |-> (y + A))
33	32	a1i 8	. . . . . . . 8 |- ((A e. RR /\ x e. RR) -> (x e. RR |-> (x + A)) = (y e. RR |-> (y + A)))
34	33	fveq1d 3732	. . . . . . 7 |- ((A e. RR /\ x e. RR) -> ((x e. RR |-> (x + A))` (x - A)) = ((y e. RR |-> (y + A))` (x - A)))
35		axaddrcl 5284	. . . . . . . . . . 11 |- (((x - A) e. RR /\ A e. RR) -> ((x - A) + A) e. RR)
36	19, 35	sylancom 477	. . . . . . . . . 10 |- ((x e. RR /\ A e. RR) -> ((x - A) + A) e. RR)
37	19, 36	jca 288	. . . . . . . . 9 |- ((x e. RR /\ A e. RR) -> ((x - A) e. RR /\ ((x - A) + A) e. RR))
38	37	ancoms 438	. . . . . . . 8 |- ((A e. RR /\ x e. RR) -> ((x - A) e. RR /\ ((x - A) + A) e. RR))
39		opreq1 3974	. . . . . . . . . 10 |- (y = (x - A) -> (y + A) = ((x - A) + A))
40	39, 30	fvopab4g 3785	. . . . . . . . 9 |- (((x - A) e. RR /\ ((x - A) + A) e. RR) -> ((y e. RR |-> (y + A))` (x - A)) = ((x - A) + A))
41		npcant 5411	. . . . . . . . . . 11 |- ((x e. CC /\ A e. CC) -> ((x - A) + A) = x)
42		recnt 5325	. . . . . . . . . . 11 |- (x e. RR -> x e. CC)
43		recnt 5325	. . . . . . . . . . 11 |- (A e. RR -> A e. CC)
44	41, 42, 43	syl2an 456	. . . . . . . . . 10 |- ((x e. RR /\ A e. RR) -> ((x - A) + A) = x)
45	44	ancoms 438	. . . . . . . . 9 |- ((A e. RR /\ x e. RR) -> ((x - A) + A) = x)
46	40, 45	sylan9eqr 1532	. . . . . . . 8 |- (((A e. RR /\ x e. RR) /\ ((x - A) e. RR /\ ((x - A) + A) e. RR)) -> ((y e. RR |-> (y + A))` (x - A)) = x)
47	38, 46	mpdan 706	. . . . . . 7 |- ((A e. RR /\ x e. RR) -> ((y e. RR |-> (y + A))` (x - A)) = x)
48	34, 47	eqtrd 1510	. . . . . 6 |- ((A e. RR /\ x e. RR) -> ((x e. RR |-> (x + A))` (x - A)) = x)
49	1, 21, 48	sylc 68	. . . . 5 |- ((A e. RR /\ x e. RR) -> (`'(x e. RR |-> (x + A))` x) = (x - A))
50		fvopab2a 10453	. . . . . 6 |- ((x e. RR /\ (x - A) e. RR) -> ((x e. RR |-> (x - A))` x) = (x - A))
51		pm3.27 323	. . . . . 6 |- ((A e. RR /\ x e. RR) -> x e. RR)
52	50, 51, 20	sylanc 473	. . . . 5 |- ((A e. RR /\ x e. RR) -> ((x e. RR |-> (x - A))` x) = (x - A))
53	49, 52	eqtr4d 1513	. . . 4 |- ((A e. RR /\ x e. RR) -> (`'(x e. RR |-> (x + A))` x) = ((x e. RR |-> (x - A))` x))
54	53	r19.21aiva 1717	. . 3 |- (A e. RR -> A.x e. RR (`'(x e. RR |-> (x + A))` x) = ((x e. RR |-> (x - A))` x))
55		eqid 1478	. . 3 |- RR = RR
56	54, 55	jctil 292	. 2 |- (A e. RR -> (RR = RR /\ A.x e. RR (`'(x e. RR |-> (x + A))` x) = ((x e. RR |-> (x - A))` x)))
57		hbcmpt 10452	. . . . 5 |- (w e. (x e. RR |-> (x + A)) -> A.x w e. (x e. RR |-> (x + A)))
58	57	hbcnv 3301	. . . 4 |- (w e. `'(x e. RR |-> (x + A)) -> A.x w e. `'(x e. RR |-> (x + A)))
59		hbcmpt 10452	. . . 4 |- (w e. (x e. RR |-> (x - A)) -> A.x w e. (x e. RR |-> (x - A)))
60	58, 59	eqfnfvf 3804	. . 3 |- ((`'(x e. RR |-> (x + A)) Fn RR /\ (x e. RR |-> (x - A)) Fn RR) -> (`'(x e. RR |-> (x + A)) = (x e. RR |-> (x - A)) <-> (RR = RR /\ A.x e. RR (`'(x e. RR |-> (x + A))` x) = ((x e. RR |-> (x - A))` x))))
61		f1o4 3702	. . . . 5 |- ((x e. RR |-> (x + A)):RR-1-1-onto->RR <-> ((x e. RR |-> (x + A)) Fn RR /\