Theorem trhom 14983

Description: In a topological group a right translation is a homeomorphism. Bourbaki TG III.2

Hypotheses

Ref	Expression
trhom.1	|- X = ran G
trhom.2	|- F = (x e. X |-> (xGA))
trhom.3	|- G = (1st` K)
trhom.4	|- J = (2nd` K)

Assertion

Ref	Expression
trhom	|- ((K e. TopGrp /\ A e. X) -> F e. (J Homeo J))

Distinct variable groups:   x,A   x,G   x,K   x,X

Proof of Theorem trhom

Step	Hyp	Ref	Expression
1		trhom.3	. . . . . 6 |- G = (1st` K)
2		trhom.4	. . . . . 6 |- J = (2nd` K)
3	1, 2	topgrpbs 14974	. . . . 5 |- (K e. TopGrp -> ran G = U.J)
4		trhom.1	. . . . . . 7 |- X = ran G
5		eqtr 1904	. . . . . . . 8 |- ((X = ran G /\ ran G = U.J) -> X = U.J)
6		f1oeq2 4631	. . . . . . . . . . 11 |- (U.J = X -> (F:U.J-1-1-onto->U.J <-> F:X-1-1-onto->U.J))
7		f1oeq3 4632	. . . . . . . . . . 11 |- (U.J = X -> (F:X-1-1-onto->U.J <-> F:X-1-1-onto->X))
8	6, 7	bitrd 587	. . . . . . . . . 10 |- (U.J = X -> (F:U.J-1-1-onto->U.J <-> F:X-1-1-onto->X))
9	8	eqcoms 1887	. . . . . . . . 9 |- (X = U.J -> (F:U.J-1-1-onto->U.J <-> F:X-1-1-onto->X))
10	9	imbi2d 674	. . . . . . . 8 |- (X = U.J -> ((A e. X -> F:U.J-1-1-onto->U.J) <-> (A e. X -> F:X-1-1-onto->X)))
11	5, 10	syl 12	. . . . . . 7 |- ((X = ran G /\ ran G = U.J) -> ((A e. X -> F:U.J-1-1-onto->U.J) <-> (A e. X -> F:X-1-1-onto->X)))
12	4, 11	mpan 759	. . . . . 6 |- (ran G = U.J -> ((A e. X -> F:U.J-1-1-onto->U.J) <-> (A e. X -> F:X-1-1-onto->X)))
13	1	topgrpgrp 14976	. . . . . . 7 |- (K e. TopGrp -> G e. Grp)
14		trhom.2	. . . . . . . . 9 |- F = (x e. X |-> (xGA))
15	14, 4	trooo 14758	. . . . . . . 8 |- ((G e. Grp /\ A e. X) -> F:X-1-1-onto->X)
16	15	ex 402	. . . . . . 7 |- (G e. Grp -> (A e. X -> F:X-1-1-onto->X))
17	13, 16	syl 12	. . . . . 6 |- (K e. TopGrp -> (A e. X -> F:X-1-1-onto->X))
18	12, 17	syl5bir 227	. . . . 5 |- (ran G = U.J -> (K e. TopGrp -> (A e. X -> F:U.J-1-1-onto->U.J)))
19	3, 18	mpcom 60	. . . 4 |- (K e. TopGrp -> (A e. X -> F:U.J-1-1-onto->U.J))
20	19	imp 377	. . 3 |- ((K e. TopGrp /\ A e. X) -> F:U.J-1-1-onto->U.J)
21		opreq12 4891	. . . . . . 7 |- ((J = (2nd` K) /\ J = (2nd` K)) -> (J Cn J) = ((2nd` K) Cn (2nd` K)))
22	21	anidms 480	. . . . . 6 |- (J = (2nd` K) -> (J Cn J) = ((2nd` K) Cn (2nd` K)))
23	22	eleq2d 1964	. . . . 5 |- (J = (2nd` K) -> (F e. (J Cn J) <-> F e. ((2nd` K) Cn (2nd` K))))
24		opelxpi 4040	. . . . . . . . . 10 |- ((x e. X /\ A e. X) -> <.x, A>. e. (X X. X))
25	24	ancoms 484	. . . . . . . . 9 |- ((A e. X /\ x e. X) -> <.x, A>. e. (X X. X))
26	25	r19.21aiva 2176	. . . . . . . 8 |- (A e. X -> A.x e. X <.x, A>. e. (X X. X))
27	26	adantl 424	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> A.x e. X <.x, A>. e. (X X. X))
28	4	grpfo 9323	. . . . . . . . 9 |- (G e. Grp -> G:(X X. X)-onto->X)
29		fofn 4619	. . . . . . . . 9 |- (G:(X X. X)-onto->X -> G Fn (X X. X))
30	13, 28, 29	3syl 24	. . . . . . . 8 |- (K e. TopGrp -> G Fn (X X. X))
31	30	adantr 425	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> G Fn (X X. X))
32		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. X /\ y = <.x, A>.)} = {<.x, y>. | (x e. X /\ y = <.x, A>.)}
33		df-mpt 5006	. . . . . . . . 9 |- (x e. X |-> (xGA)) = {<.x, y>. | (x e. X /\ y = (xGA))}
34		df-opr 4886	. . . . . . . . . . . 12 |- (xGA) = (G` <.x, A>.)
35	34	eqeq2i 1894	. . . . . . . . . . 11 |- (y = (xGA) <-> y = (G` <.x, A>.))
36	35	anbi2i 538	. . . . . . . . . 10 |- ((x e. X /\ y = (xGA)) <-> (x e. X /\ y = (G` <.x, A>.)))
37	36	opabbii 3402	. . . . . . . . 9 |- {<.x, y>. | (x e. X /\ y = (xGA))} = {<.x, y>. | (x e. X /\ y = (G` <.x, A>.))}
38	14, 33, 37	3eqtri 1912	. . . . . . . 8 |- F = {<.x, y>. | (x e. X /\ y = (G` <.x, A>.))}
39	32, 38	fnopabco2b 14734	. . . . . . 7 |- ((A.x e. X <.x, A>. e. (X X. X) /\ G Fn (X X. X)) -> F = (G o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}))
40	27, 31, 39	syl11anc 524	. . . . . 6 |- ((K e. TopGrp /\ A e. X) -> F = (G o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}))
41		eqid 1884	. . . . . . . . . 10 |- (2nd` K) = (2nd` K)
42	41	topgrptop 14977	. . . . . . . . 9 |- (K e. TopGrp -> (2nd` K) e. Top)
43		eqid 1884	. . . . . . . . . . 11 |- ((2nd` K) X.t (2nd` K)) = ((2nd` K) X.t (2nd` K))
44	43	txtop 8934	. . . . . . . . . 10 |- (((2nd` K) e. Top /\ (2nd` K) e. Top) -> ((2nd` K) X.t (2nd` K)) e. Top)
45	42, 42, 44	syl11anc 524	. . . . . . . . 9 |- (K e. TopGrp -> ((2nd` K) X.t (2nd` K)) e. Top)
46	42, 45, 42	3jca 1050	. . . . . . . 8 |- (K e. TopGrp -> ((2nd` K) e. Top /\ ((2nd` K) X.t (2nd` K)) e. Top /\ (2nd` K) e. Top))
47	46	adantr 425	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> ((2nd` K) e. Top /\ ((2nd` K) X.t (2nd` K)) e. Top /\ (2nd` K) e. Top))
48	4	eqcomi 1888	. . . . . . . . . . 11 |- ran G = X
49	2	unieqi 3187	. . . . . . . . . . 11 |- U.J = U.(2nd` K)
50	48, 49	eqeq12i 1897	. . . . . . . . . 10 |- (ran G = U.J <-> X = U.(2nd` K))
51	50	biimpi 168	. . . . . . . . 9 |- (ran G = U.J -> X = U.(2nd` K))
52		eqid 1884	. . . . . . . . . . . 12 |- U.(2nd` K) = U.(2nd` K)
53		eqid 1884	. . . . . . . . . . . 12 |- {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)} = {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)}
54	52, 53	ttcn 14913	. . . . . . . . . . 11 |- (((2nd` K) e. Top /\ A e. U.(2nd` K)) -> {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))))
55	54, 42	sylan 497	. . . . . . . . . 10 |- ((K e. TopGrp /\ A e. U.(2nd` K)) -> {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))))
56		eleq2 1958	. . . . . . . . . . . 12 |- (X = U.(2nd` K) -> (A e. X <-> A e. U.(2nd` K)))
57	56	anbi2d 678	. . . . . . . . . . 11 |- (X = U.(2nd` K) -> ((K e. TopGrp /\ A e. X) <-> (K e. TopGrp /\ A e. U.(2nd` K))))
58		ax-17 1317	. . . . . . . . . . . . 13 |- (X = U.(2nd` K) -> A.x X = U.(2nd` K))
59		ax-17 1317	. . . . . . . . . . . . 13 |- (X = U.(2nd` K) -> A.y X = U.(2nd` K))
60		eleq2 1958	. . . . . . . . . . . . . 14 |- (X = U.(2nd` K) -> (x e. X <-> x e. U.(2nd` K)))
61	60	anbi1d 679	. . . . . . . . . . . . 13 |- (X = U.(2nd` K) -> ((x e. X /\ y = <.x, A>.) <-> (x e. U.(2nd` K) /\ y = <.x, A>.)))
62	58, 59, 61	opabbid 3399	. . . . . . . . . . . 12 |- (X = U.(2nd` K) -> {<.x, y>. | (x e. X /\ y = <.x, A>.)} = {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)})
63	62	eleq1d 1963	. . . . . . . . . . 11 |- (X = U.(2nd` K) -> ({<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))) <-> {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K)))))
64	57, 63	imbi12d 688	. . . . . . . . . 10 |- (X = U.(2nd` K) -> (((K e. TopGrp /\ A e. X) -> {<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K)))) <-> ((K e. TopGrp /\ A e. U.(2nd` K)) -> {<.x, y>. | (x e. U.(2nd` K) /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))))))
65	55, 64	mpbiri 211	. . . . . . . . 9 |- (X = U.(2nd` K) -> ((K e. TopGrp /\ A e. X) -> {<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K)))))
66	3, 51, 65	3syl 24	. . . . . . . 8 |- (K e. TopGrp -> ((K e. TopGrp /\ A e. X) -> {<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K)))))
67	66	anabsi5 553	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> {<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))))
68	1, 41	topgrpcn 14975	. . . . . . . 8 |- (K e. TopGrp -> G e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))
69	68	adantr 425	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> G e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))
70		cnco 9045	. . . . . . 7 |- ((((2nd` K) e. Top /\ ((2nd` K) X.t (2nd` K)) e. Top /\ (2nd` K) e. Top) /\ ({<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))) /\ G e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))) -> (G o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}) e. ((2nd` K) Cn (2nd` K)))
71	47, 67, 69, 70	syl12anc 1098	. . . . . 6 |- ((K e. TopGrp /\ A e. X) -> (G o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}) e. ((2nd` K) Cn (2nd` K)))
72	40, 71	eqeltrd 1971	. . . . 5 |- ((K e. TopGrp /\ A e. X) -> F e. ((2nd` K) Cn (2nd` K)))
73	23, 72	syl5bir 227	. . . 4 |- (J = (2nd` K) -> ((K e. TopGrp /\ A e. X) -> F e. (J Cn J)))
74	2, 73	ax-mp 7	. . 3 |- ((K e. TopGrp /\ A e. X) -> F e. (J Cn J))
75		eqid 1884	. . . . . 6 |- ( /g ` G) = ( /g ` G)
76	14, 4, 75	trinv 14759	. . . . 5 |- ((G e. Grp /\ A e. X) -> `'F = (x e. X |-> (x( /g ` G)A)))
77	76, 13	sylan 497	. . . 4 |- ((K e. TopGrp /\ A e. X) -> `'F = (x e. X |-> (x( /g ` G)A)))
78	22	eleq2d 1964	. . . . . 6 |- (J = (2nd` K) -> ((x e. X |-> (x( /g ` G)A)) e. (J Cn J) <-> (x e. X |-> (x( /g ` G)A)) e. ((2nd` K) Cn (2nd` K))))
79	4, 75	grpdivfo 14737	. . . . . . . . . 10 |- (G e. Grp -> ( /g ` G):(X X. X)-onto->X)
80		fofn 4619	. . . . . . . . . 10 |- (( /g ` G):(X X. X)-onto->X -> ( /g ` G) Fn (X X. X))
81	13, 79, 80	3syl 24	. . . . . . . . 9 |- (K e. TopGrp -> ( /g ` G) Fn (X X. X))
82	81	adantr 425	. . . . . . . 8 |- ((K e. TopGrp /\ A e. X) -> ( /g ` G) Fn (X X. X))
83		df-mpt 5006	. . . . . . . . . 10 |- (x e. X |-> (x( /g ` G)A)) = {<.x, y>. | (x e. X /\ y = (x( /g ` G)A))}
84		df-opr 4886	. . . . . . . . . . . . 13 |- (x( /g ` G)A) = (( /g ` G)` <.x, A>.)
85	84	eqeq2i 1894	. . . . . . . . . . . 12 |- (y = (x( /g ` G)A) <-> y = (( /g ` G)` <.x, A>.))
86	85	anbi2i 538	. . . . . . . . . . 11 |- ((x e. X /\ y = (x( /g ` G)A)) <-> (x e. X /\ y = (( /g ` G)` <.x, A>.)))
87	86	opabbii 3402	. . . . . . . . . 10 |- {<.x, y>. | (x e. X /\ y = (x( /g ` G)A))} = {<.x, y>. | (x e. X /\ y = (( /g ` G)` <.x, A>.))}
88	83, 87	eqtri 1908	. . . . . . . . 9 |- (x e. X |-> (x( /g ` G)A)) = {<.x, y>. | (x e. X /\ y = (( /g ` G)` <.x, A>.))}
89	32, 88	fnopabco2b 14734	. . . . . . . 8 |- ((A.x e. X <.x, A>. e. (X X. X) /\ ( /g ` G) Fn (X X. X)) -> (x e. X |-> (x( /g ` G)A)) = (( /g ` G) o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}))
90	27, 82, 89	syl11anc 524	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> (x e. X |-> (x( /g ` G)A)) = (( /g ` G) o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}))
91	1, 41, 75	topgrpsubcn 14982	. . . . . . . . 9 |- (K e. TopGrp -> ( /g ` G) e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))
92	91	adantr 425	. . . . . . . 8 |- ((K e. TopGrp /\ A e. X) -> ( /g ` G) e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))
93		cnco 9045	. . . . . . . 8 |- ((((2nd` K) e. Top /\ ((2nd` K) X.t (2nd` K)) e. Top /\ (2nd` K) e. Top) /\ ({<.x, y>. | (x e. X /\ y = <.x, A>.)} e. ((2nd` K) Cn ((2nd` K) X.t (2nd` K))) /\ ( /g ` G) e. (((2nd` K) X.t (2nd` K)) Cn (2nd` K)))) -> (( /g ` G) o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}) e. ((2nd` K) Cn (2nd` K)))
94	47, 67, 92, 93	syl12anc 1098	. . . . . . 7 |- ((K e. TopGrp /\ A e. X) -> (( /g ` G) o. {<.x, y>. | (x e. X /\ y = <.x, A>.)}) e. ((2nd` K) Cn (2nd` K)))
95	90, 94	eqeltrd 1971	. . . . . 6 |- ((K e. TopGrp /\ A e. X) -> (x e. X |-> (x( /g ` G)A)) e. ((2nd` K) Cn (2nd` K)))
96	78, 95	syl5bir 227	. . . . 5 |- (J = (2nd` K) -> ((K e. TopGrp /\ A e. X) -> (x e. X |-> (x( /g ` G)A)) e. (J Cn J)))
97	2, 96	ax-mp 7	. . . 4 |- ((K e. TopGrp /\ A e. X) -> (x e. X |-> (x( /g ` G)A)) e. (J Cn J))
98	77, 97	eqeltrd 1971	. . 3 |- ((K e. TopGrp /\ A e. X) -> `'F e. (J Cn J))
99	20, 74, 98	3jca 1050	. 2 |- ((K e. TopGrp /\ A e. X) -> (F:U.J-1-1-onto->U.J /\ F e. (J Cn J) /\ `'F e. (J Cn J)))
100	2	topgrptop 14977	. . . 4 |- (K e. TopGrp -> J e. Top)
101	100	adantr 425	. . 3 |- ((K e. TopGrp /\ A e. X) -> J e. Top)
102		fex 4595	. . . 4 |- ((F:X-->_V /\ X e. _V) -> F e. _V)
103		oprex 4907	. . . . . . 7 |- (xGA) e. _V
104	103	a1i 8	. . . . . 6 |- (x e. X -> (xGA) e. _V)
105	104	rgen 2159	. . . . 5 |- A.x e. X (xGA) e. _V
106	14	fopab2a 14479	. . . . 5 |- (A.x e. X (xGA) e. _V <-> F:X-->_V)
107	105, 106	mpbi 206	. . . 4 |- F:X-->_V
108		fvex 4689	. . . . . . . 8 |- (1st` K) e. _V
109	1, 108	eqeltri 1967	. . . . . . 7 |- G e. _V
110	109	rnex 4209	. . . . . 6 |- ran G e. _V
111	4, 110	eqeltri 1967	. . . . 5 |- X e. _V
112	111	a1i 8	. . . 4 |- ((K e. TopGrp /\ A e. X) -> X e. _V)
113	102, 107, 112	sylancr 526	. . 3 |- ((K e. TopGrp /\ A e. X) -> F e. _V)
114		eqid 1884	. . . 4 |- U.J = U.J
115	114, 114	hmeobc 10239	. . 3 |- ((J e. Top /\ J e. Top /\ F e. _V) -> (F e. (J Homeo J) <-> (F:U.J-1-1-onto->U.J /\ F e. (J Cn J) /\ `'F e. (J Cn J))))
116	101, 101, 113, 115	syl111anc 1100	. 2 |- ((K e. TopGrp /\ A e. X) -> (F e. (J Homeo J) <-> (F:U.J-1-1-onto->U.J /\ F e. (J Cn J) /\ `'F e. (J Cn J))))
117	99, 116	mpbird 213	1 |- ((K e. TopGrp /\ A e. X) -> F e. (J Homeo J))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292  <.cop 3046  U.cuni 3177  {copab 3395   X. cxp 3984  `'ccnv 3985  ran crn 3987   o. ccom 3990   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884   e. cmpt 5004  1stc1st 5018  2ndc2nd 5019  Topctop 8857   X.t ctx 8930   Cn ccn 9028  Grpcgr 9311   /g cgs 9314   Homeo chomeosm 10230  TopGrpctopgrp 14969

This theorem is referenced by:  cnvtrhom 14984  trhom2 14985

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-map 5383  df-top 8861  df-bases 8863  df-topgen 8864  df-tx 8931  df-cn 9030  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-homeo 10232  df-topgrp 14970

Copyright terms: Public domain