Theorem hmeogrp 10461

Description: Homeomorphisms on a topology J is a group for composition. This means from Felix Klein's point of view that a set equipped with a topology is a geometry, namely the rubber sheet geometry.

Assertion

Ref	Expression
hmeogrp	|- (J e. Top -> {<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))} e. Grp)

Distinct variable group:   x,J,y,z

Proof of Theorem hmeogrp

Step	Hyp	Ref	Expression
1		cmphmp 10444	. . . . . . . . 9 |- ((J e. Top /\ J e. Top /\ J e. Top) -> ((y e. (J Homeo J) /\ x e. (J Homeo J)) -> (x o. y) e. (J Homeo J)))
2	1	ancomsd 437	. . . . . . . 8 |- ((J e. Top /\ J e. Top /\ J e. Top) -> ((x e. (J Homeo J) /\ y e. (J Homeo J)) -> (x o. y) e. (J Homeo J)))
3	2	3exp 831	. . . . . . 7 |- (J e. Top -> (J e. Top -> (J e. Top -> ((x e. (J Homeo J) /\ y e. (J Homeo J)) -> (x o. y) e. (J Homeo J)))))
4	3	pm2.43d 65	. . . . . 6 |- (J e. Top -> (J e. Top -> ((x e. (J Homeo J) /\ y e. (J Homeo J)) -> (x o. y) e. (J Homeo J))))
5	4	pm2.43i 64	. . . . 5 |- (J e. Top -> ((x e. (J Homeo J) /\ y e. (J Homeo J)) -> (x o. y) e. (J Homeo J)))
6	5	r19.21aivv 1717	. . . 4 |- (J e. Top -> A.x e. (J Homeo J)A.y e. (J Homeo J)(x o. y) e. (J Homeo J))
7		df-3an 776	. . . . . 6 |- ((x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y)) <-> ((x e. (J Homeo J) /\ y e. (J Homeo J)) /\ z = (x o. y)))
8	7	oprabbii 3988	. . . . 5 |- {<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))} = {<.<.x, y>., z>. | ((x e. (J Homeo J) /\ y e. (J Homeo J)) /\ z = (x o. y))}
9	8	foprab2 4109	. . . 4 |- (A.x e. (J Homeo J)A.y e. (J Homeo J)(x o. y) e. (J Homeo J) <-> {<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}:((J Homeo J) X. (J Homeo J))-->(J Homeo J))
10	6, 9	sylib 198	. . 3 |- (J e. Top -> {<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}:((J Homeo J) X. (J Homeo J))-->(J Homeo J))
11		coass 3504	. . . . . . . . 9 |- ((a o. b) o. c) = (a o. (b o. c))
12		coeq1 3276	. . . . . . . . . . . . 13 |- (x = a -> (x o. y) = (a o. y))
13		coeq2 3277	. . . . . . . . . . . . 13 |- (y = b -> (a o. y) = (a o. b))
14	12, 13, 8	oprabval2g 4018	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ (a o. b) e. V) -> (a{<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}b) = (a o. b))
15	14	opreq1d 3966	. . . . . . . . . . 11 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ (a o. b) e. V) -> ((a{<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c) = ((a o. b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c))
16		3simp1 787	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> a e. (J Homeo J))
17	16	adantl 388	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> a e. (J Homeo J))
18		3simp2 788	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> b e. (J Homeo J))
19	18	adantl 388	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> b e. (J Homeo J))
20		coexg 3516	. . . . . . . . . . . . 13 |- ((a e. (J Homeo J) /\ b e. (J Homeo J)) -> (a o. b) e. V)
21	20	3adant3 798	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> (a o. b) e. V)
22	21	adantl 388	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> (a o. b) e. V)
23	15, 17, 19, 22	syl3anc 857	. . . . . . . . . 10 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> ((a{<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c) = ((a o. b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c))
24		coeq1 3276	. . . . . . . . . . . 12 |- (x = (a o. b) -> (x o. y) = ((a o. b) o. y))
25		coeq2 3277	. . . . . . . . . . . 12 |- (y = c -> ((a o. b) o. y) = ((a o. b) o. c))
26	24, 25, 8	oprabval2g 4018	. . . . . . . . . . 11 |- (((a o. b) e. (J Homeo J) /\ c e. (J Homeo J) /\ ((a o. b) o. c) e. V) -> ((a o. b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c) = ((a o. b) o. c))
27		cmphmp 10444	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ J e. Top /\ J e. Top) -> ((b e. (J Homeo J) /\ a e. (J Homeo J)) -> (a o. b) e. (J Homeo J)))
28	27	3exp 831	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> (J e. Top -> (J e. Top -> ((b e. (J Homeo J) /\ a e. (J Homeo J)) -> (a o. b) e. (J Homeo J)))))
29	28	pm2.43d 65	. . . . . . . . . . . . . . . 16 |- (J e. Top -> (J e. Top -> ((b e. (J Homeo J) /\ a e. (J Homeo J)) -> (a o. b) e. (J Homeo J))))
30	29	pm2.43i 64	. . . . . . . . . . . . . . 15 |- (J e. Top -> ((b e. (J Homeo J) /\ a e. (J Homeo J)) -> (a o. b) e. (J Homeo J)))
31	30	com12 11	. . . . . . . . . . . . . 14 |- ((b e. (J Homeo J) /\ a e. (J Homeo J)) -> (J e. Top -> (a o. b) e. (J Homeo J)))
32	31	ancoms 436	. . . . . . . . . . . . 13 |- ((a e. (J Homeo J) /\ b e. (J Homeo J)) -> (J e. Top -> (a o. b) e. (J Homeo J)))
33	32	3adant3 798	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> (J e. Top -> (a o. b) e. (J Homeo J)))
34	33	impcom 351	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> (a o. b) e. (J Homeo J))
35		3simp3 789	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> c e. (J Homeo J))
36	35	adantl 388	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> c e. (J Homeo J))
37		coexg 3516	. . . . . . . . . . . . 13 |- (((a o. b) e. V /\ c e. (J Homeo J)) -> ((a o. b) o. c) e. V)
38	37, 21, 35	sylanc 471	. . . . . . . . . . . 12 |- ((a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J)) -> ((a o. b) o. c) e. V)
39	38	adantl 388	. . . . . . . . . . 11 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> ((a o. b) o. c) e. V)
40	26, 34, 36, 39	syl3anc 857	. . . . . . . . . 10 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> ((a o. b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c) = ((a o. b) o. c))
41	23, 40	eqtrd 1504	. . . . . . . . 9 |- ((J e. Top /\ (a e. (J Homeo J) /\ b e. (J Homeo J) /\ c e. (J Homeo J))) -> ((a{<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}b){<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))}c) = ((a o. b) o. c))
42		coeq1 3276	. . . . . . . . . . . . 13 |- (x = b -> (x o. y) = (b o. y))
43		coeq2 3277	. . . . . . . . . . . . 13 |- (y = c -> (b o. y) = (b o. c))
44	42, 43, 8	oprabval2g 4018	. . . . . . . . . . . 12 |-