Table of ContentsTable of Contents Mathbox for Frédéric Liné < Previous   Next >
Related theorems
Unicode version
Theorem curgrpact 14735
Description: The currying of a group action is a group homomorphism between the group G and the symetry group (SymGrp` ran M).
Hypotheses
Ref Expression
curgrpact.1 |- M e. A
curgrpact.2 |- ran M =/= (/)
Assertion
Ref Expression
curgrpact |- (<.G, M>. e. GrpAct -> (cur1` M) e. (G GrpHom (SymGrp` ran M)))
Proof of Theorem curgrpact
StepHypRef Expression
1 curgrpact.1 . 2 |- M e. A
2 eqid 1884 . . . 4 |- ran G = ran G
3 eqid 1884 . . . 4 |- ran M = ran M
4 eqid 1884 . . . 4 |- (Id` G) = (Id` G)
52, 3, 4isga2 9452 . . 3 |- (M e. A -> (<.G, M>. e. GrpAct <-> (G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))))
6 rnexg 4207 . . . . . . . . . . . 12 |- (G e. Grp -> ran G e. _V)
763ad2ant1 897 . . . . . . . . . . 11 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ran G e. _V)
8 rnexg 4207 . . . . . . . . . . . . 13 |- (M e. A -> ran M e. _V)
91, 8ax-mp 7 . . . . . . . . . . . 12 |- ran M e. _V
109a1i 8 . . . . . . . . . . 11 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ran M e. _V)
11 ffn 4562 . . . . . . . . . . . . 13 |- (M:(ran G X. ran M)-->ran M -> M Fn (ran G X. ran M))
12113ad2ant2 898 . . . . . . . . . . . 12 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> M Fn (ran G X. ran M))
13 curgrpact.2 . . . . . . . . . . . 12 |- ran M =/= (/)
1412, 13jctil 316 . . . . . . . . . . 11 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (ran M =/= (/) /\ M Fn (ran G X. ran M)))
157, 10, 14jca31 311 . . . . . . . . . 10 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M))))
16 domrancur1c 14550 . . . . . . . . . 10 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M))) -> (cur1` M):ran G-->{z | z:ran M-->ran M})
17 ffun 4565 . . . . . . . . . 10 |- ((cur1` M):ran G-->{z | z:ran M-->ran M} -> Fun (cur1` M))
1815, 16, 173syl 24 . . . . . . . . 9 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> Fun (cur1` M))
197, 10, 14, 16syl21anc 1099 . . . . . . . . . 10 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (cur1` M):ran G-->{z | z:ran M-->ran M})
20 fdm 4567 . . . . . . . . . 10 |- ((cur1` M):ran G-->{z | z:ran M-->ran M} -> dom (cur1` M) = ran G)
2119, 20syl 12 . . . . . . . . 9 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> dom (cur1` M) = ran G)
2218, 21jca 310 . . . . . . . 8 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (Fun (cur1` M) /\ dom (cur1` M) = ran G))
23 df-fn 4009 . . . . . . . 8 |- ((cur1` M) Fn ran G <-> (Fun (cur1` M) /\ dom (cur1` M) = ran G))
2422, 23sylibr 217 . . . . . . 7 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (cur1` M) Fn ran G)
257, 9jctir 317 . . . . . . . . . . . . . . 15 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (ran G e. _V /\ ran M e. _V))
2625adantr 425 . . . . . . . . . . . . . 14 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> (ran G e. _V /\ ran M e. _V))
2712adantr 425 . . . . . . . . . . . . . . 15 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> M Fn (ran G X. ran M))
2827, 13jctil 316 . . . . . . . . . . . . . 14 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> (ran M =/= (/) /\ M Fn (ran G X. ran M)))
29 simpr 350 . . . . . . . . . . . . . 14 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> a e. ran G)
3026, 28, 293jca 1050 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> ((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ a e. ran G))
31 valcurfn 14551 . . . . . . . . . . . . 13 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ a e. ran G) -> ((cur1` M)` a):ran M-->ran M)
32 ffn 4562 . . . . . . . . . . . . 13 |- (((cur1` M)` a):ran M-->ran M -> ((cur1` M)` a) Fn ran M)
3330, 31, 323syl 24 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> ((cur1` M)` a) Fn ran M)
341a1i 8 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> M e. A)
355bicomd 580 . . . . . . . . . . . . . . . 16 |- (M e. A -> ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) <-> <.G, M>. e. GrpAct))
361, 35ax-mp 7 . . . . . . . . . . . . . . 15 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) <-> <.G, M>. e. GrpAct)
3736biimpi 168 . . . . . . . . . . . . . 14 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> <.G, M>. e. GrpAct)
3837adantr 425 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> <.G, M>. e. GrpAct)
3929, 13jctir 317 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> (a e. ran G /\ ran M =/= (/)))
402, 3rngapm 14733 . . . . . . . . . . . . 13 |- ((M e. A /\ <.G, M>. e. GrpAct /\ (a e. ran G /\ ran M =/= (/))) -> ran ((cur1` M)` a) = ran M)
4134, 38, 39, 40syl111anc 1100 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> ran ((cur1` M)` a) = ran M)
42 ax-17 1317 . . . . . . . . . . . . . . 15 |- (G e. Grp -> A.x G e. Grp)
43 ax-17 1317 . . . . . . . . . . . . . . 15 |- (M:(ran G X. ran M)-->ran M -> A.x M:(ran G X. ran M)-->ran M)
44 ax-17 1317 . . . . . . . . . . . . . . . 16 |- (f e. ran M -> A.x f e. ran M)
45 ax-17 1317 . . . . . . . . . . . . . . . . 17 |- (((Id` G)Mf) = f -> A.x((Id` G)Mf) = f)
46 hbra1 2147 . . . . . . . . . . . . . . . . 17 |- (A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)) -> A.xA.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))
4745, 46hban 1356 . . . . . . . . . . . . . . . 16 |- ((((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) -> A.x(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))
4844, 47hbral 2146 . . . . . . . . . . . . . . 15 |- (A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) -> A.xA.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))
4942, 43, 48hb3an 1359 . . . . . . . . . . . . . 14 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> A.x(G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))))
50 ax-17 1317 . . . . . . . . . . . . . 14 |- (a e. ran G -> A.x a e. ran G)
5149, 50hban 1356 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> A.x((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G))
52 ax-17 1317 . . . . . . . . . . . . . . . . . 18 |- (G e. Grp -> A.y G e. Grp)
53 ax-17 1317 . . . . . . . . . . . . . . . . . 18 |- (M:(ran G X. ran M)-->ran M -> A.y M:(ran G X. ran M)-->ran M)
54 ax-17 1317 . . . . . . . . . . . . . . . . . . 19 |- (f e. ran M -> A.y f e. ran M)
55 ax-17 1317 . . . . . . . . . . . . . . . . . . . 20 |- (((Id` G)Mf) = f -> A.y((Id` G)Mf) = f)
56 ax-17 1317 . . . . . . . . . . . . . . . . . . . . 21 |- (x e. ran G -> A.y x e. ran G)
57 hbra1 2147 . . . . . . . . . . . . . . . . . . . . 21 |- (A.y e. ran G((xGy)Mf) = (xM(yMf)) -> A.yA.y e. ran G((xGy)Mf) = (xM(yMf)))
5856, 57hbral 2146 . . . . . . . . . . . . . . . . . . . 20 |- (A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)) -> A.yA.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))
5955, 58hban 1356 . . . . . . . . . . . . . . . . . . 19 |- ((((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) -> A.y(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))
6054, 59hbral 2146 . . . . . . . . . . . . . . . . . 18 |- (A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) -> A.yA.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))
6152, 53, 60hb3an 1359 . . . . . . . . . . . . . . . . 17 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> A.y(G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))))
62 ax-17 1317 . . . . . . . . . . . . . . . . 17 |- (a e. ran G -> A.y a e. ran G)
6361, 62hban 1356 . . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> A.y((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G))
64 ax-17 1317 . . . . . . . . . . . . . . . 16 |- (x e. ran M -> A.y x e. ran M)
6563, 64hban 1356 . . . . . . . . . . . . . . 15 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) -> A.y(((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M))
6626ad2antrr 440 . . . . . . . . . . . . . . . . . 18 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> (ran G e. _V /\ ran M e. _V))
6728ad2antrr 440 . . . . . . . . . . . . . . . . . 18 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> (ran M =/= (/) /\ M Fn (ran G X. ran M)))
68 simpllr 453 . . . . . . . . . . . . . . . . . . 19 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> a e. ran G)
69 simplr 449 . . . . . . . . . . . . . . . . . . 19 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> x e. ran M)
7068, 69jca 310 . . . . . . . . . . . . . . . . . 18 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> (a e. ran G /\ x e. ran M))
71 simpr 350 . . . . . . . . . . . . . . . . . . 19 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> y e. ran M)
7268, 71jca 310 . . . . . . . . . . . . . . . . . 18 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> (a e. ran G /\ y e. ran M))
73 valvalcurfn 14554 . . . . . . . . . . . . . . . . . . 19 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ (a e. ran G /\ x e. ran M)) -> (((cur1` M)` a)` x) = (aMx))
74 valvalcurfn 14554 . . . . . . . . . . . . . . . . . . 19 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ (a e. ran G /\ y e. ran M)) -> (((cur1` M)` a)` y) = (aMy))
7573, 74anim12i 360 . . . . . . . . . . . . . . . . . 18 |- ((((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ (a e. ran G /\ x e. ran M)) /\ ((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ (a e. ran G /\ y e. ran M))) -> ((((cur1` M)` a)` x) = (aMx) /\ (((cur1` M)` a)` y) = (aMy)))
7666, 67, 70, 66, 67, 72, 75syl33anc 1115 . . . . . . . . . . . . . . . . 17 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> ((((cur1` M)` a)` x) = (aMx) /\ (((cur1` M)` a)` y) = (aMy)))
77 eqeq12 1896 . . . . . . . . . . . . . . . . . . 19 |- (((((cur1` M)` a)` x) = (aMx) /\ (((cur1` M)` a)` y) = (aMy)) -> ((((cur1` M)` a)` x) = (((cur1` M)` a)` y) <-> (aMx) = (aMy)))
7877biimpd 170 . . . . . . . . . . . . . . . . . 18 |- (((((cur1` M)` a)` x) = (aMx) /\ (((cur1` M)` a)` y) = (aMy)) -> ((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> (aMx) = (aMy)))
791elisseti 2301 . . . . . . . . . . . . . . . . . . . 20 |- M e. _V
8079a1i 8 . . . . . . . . . . . . . . . . . . 19 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> M e. _V)
8138ad2antrr 440 . . . . . . . . . . . . . . . . . . 19 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> <.G, M>. e. GrpAct)
822, 3gaplc 14731 . . . . . . . . . . . . . . . . . . 19 |- ((M e. _V /\ <.G, M>. e. GrpAct /\ (a e. ran G /\ x e. ran M /\ y e. ran M)) -> ((aMx) = (aMy) -> x = y))
8380, 81, 68, 69, 71, 82syl113anc 1112 . . . . . . . . . . . . . . . . . 18 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> ((aMx) = (aMy) -> x = y))
8478, 83syl9r 72 . . . . . . . . . . . . . . . . 17 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> (((((cur1` M)` a)` x) = (aMx) /\ (((cur1` M)` a)` y) = (aMy)) -> ((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y)))
8576, 84mpd 29 . . . . . . . . . . . . . . . 16 |- (((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) /\ y e. ran M) -> ((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y))
8685ex 402 . . . . . . . . . . . . . . 15 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) -> (y e. ran M -> ((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y)))
8765, 86r19.21ai 2174 . . . . . . . . . . . . . 14 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) /\ x e. ran M) -> A.y e. ran M((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y))
8887ex 402 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> (x e. ran M -> A.y e. ran M((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y)))
8951, 88r19.21ai 2174 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> A.x e. ran MA.y e. ran M((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y))
9033, 41, 893jca 1050 . . . . . . . . . . 11 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> (((cur1` M)` a) Fn ran M /\ ran ((cur1` M)` a) = ran M /\ A.x e. ran MA.y e. ran M((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y)))
91 dff1o6 4853 . . . . . . . . . . 11 |- (((cur1` M)` a):ran M-1-1-onto->ran M <-> (((cur1` M)` a) Fn ran M /\ ran ((cur1` M)` a) = ran M /\ A.x e. ran MA.y e. ran M((((cur1` M)` a)` x) = (((cur1` M)` a)` y) -> x = y)))
9290, 91sylibr 217 . . . . . . . . . 10 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> ((cur1` M)` a):ran M-1-1-onto->ran M)
93 fvex 4689 . . . . . . . . . . 11 |- ((cur1` M)` a) e. _V
94 f1oeq1 4630 . . . . . . . . . . 11 |- (f = ((cur1` M)` a) -> (f:ran M-1-1-onto->ran M <-> ((cur1` M)` a):ran M-1-1-onto->ran M))
9593, 94elab 2403 . . . . . . . . . 10 |- (((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M} <-> ((cur1` M)` a):ran M-1-1-onto->ran M)
9692, 95sylibr 217 . . . . . . . . 9 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ a e. ran G) -> ((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M})
9796ex 402 . . . . . . . 8 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (a e. ran G -> ((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M}))
9897r19.21aiv 2175 . . . . . . 7 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> A.a e. ran G((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M})
9924, 98jca 310 . . . . . 6 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((cur1` M) Fn ran G /\ A.a e. ran G((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M}))
100 ffnfv 4801 . . . . . 6 |- ((cur1` M):ran G-->{f | f:ran M-1-1-onto->ran M} <-> ((cur1` M) Fn ran G /\ A.a e. ran G((cur1` M)` a) e. {f | f:ran M-1-1-onto->ran M}))
10199, 100sylibr 217 . . . . 5 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (cur1` M):ran G-->{f | f:ran M-1-1-onto->ran M})
10261, 56hban 1356 . . . . . . . 8 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ x e. ran G) -> A.y((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ x e. ran G))
10325adantr 425 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (ran G e. _V /\ ran M e. _V))
10414adantr 425 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (ran M =/= (/) /\ M Fn (ran G X. ran M)))
105 simprl 450 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> x e. ran G)
106 valcurfn2 14553 . . . . . . . . . . . . 13 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ x e. ran G) -> ((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))})
107103, 104, 105, 106syl111anc 1100 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))})
108 simprr 451 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> y e. ran G)
109 valcurfn2 14553 . . . . . . . . . . . . 13 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ y e. ran G) -> ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))})
110103, 104, 108, 109syl111anc 1100 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))})
1112grpcl 9324 . . . . . . . . . . . . . . . 16 |- ((G e. Grp /\ x e. ran G /\ y e. ran G) -> (xGy) e. ran G)
1121113expib 1070 . . . . . . . . . . . . . . 15 |- (G e. Grp -> ((x e. ran G /\ y e. ran G) -> (xGy) e. ran G))
1131123ad2ant1 897 . . . . . . . . . . . . . 14 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((x e. ran G /\ y e. ran G) -> (xGy) e. ran G))
114113imp 377 . . . . . . . . . . . . 13 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (xGy) e. ran G)
115 valcurfn2 14553 . . . . . . . . . . . . 13 |- (((ran G e. _V /\ ran M e. _V) /\ (ran M =/= (/) /\ M Fn (ran G X. ran M)) /\ (xGy) e. ran G) -> ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})
116103, 104, 114, 115syl111anc 1100 . . . . . . . . . . . 12 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})
117107, 110, 1163jca 1050 . . . . . . . . . . 11 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))}))
118 opreq12 4891 . . . . . . . . . . . . . 14 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))}) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}))
1191183adant3 896 . . . . . . . . . . . . 13 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))}) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}))
120119adantl 424 . . . . . . . . . . . 12 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}))
121 simpl 346 . . . . . . . . . . . . . . . . . . . 20 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> ((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))})
1221a1i 8 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> M e. A)
12337adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> <.G, M>. e. GrpAct)
124105, 13jctir 317 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (x e. ran G /\ ran M =/= (/)))
1252, 3gapm2 14732 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((M e. A /\ <.G, M>. e. GrpAct /\ (x e. ran G /\ ran M =/= (/))) -> ((cur1` M)` x):ran M-1-1-onto->ran M)
126122, 123, 124, 125syl111anc 1100 . . . . . . . . . . . . . . . . . . . . . 22 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` x):ran M-1-1-onto->ran M)
127 fvex 4689 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((cur1` M)` x) e. _V
128 f1oeq1 4630 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = ((cur1` M)` x) -> (z:ran M-1-1-onto->ran M <-> ((cur1` M)` x):ran M-1-1-onto->ran M))
129128elabg 2405 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((cur1` M)` x) e. _V -> (((cur1` M)` x) e. {z | z:ran M-1-1-onto->ran M} <-> ((cur1` M)` x):ran M-1-1-onto->ran M))
130127, 129ax-mp 7 . . . . . . . . . . . . . . . . . . . . . 22 |- (((cur1` M)` x) e. {z | z:ran M-1-1-onto->ran M} <-> ((cur1` M)` x):ran M-1-1-onto->ran M)
131126, 130sylibr 217 . . . . . . . . . . . . . . . . . . . . 21 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` x) e. {z | z:ran M-1-1-onto->ran M})
132131adantl 424 . . . . . . . . . . . . . . . . . . . 20 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> ((cur1` M)` x) e. {z | z:ran M-1-1-onto->ran M})
133121, 132eqeltrrd 1972 . . . . . . . . . . . . . . . . . . 19 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> {<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M})
134133adantlr 429 . . . . . . . . . . . . . . . . . 18 |- (((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))}) /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> {<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M})
135 simpl 346 . . . . . . . . . . . . . . . . . . . 20 |- ((((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))})
136108, 13jctir 317 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (y e. ran G /\ ran M =/= (/)))
1372, 3gapm2 14732 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((M e. A /\ <.G, M>. e. GrpAct /\ (y e. ran G /\ ran M =/= (/))) -> ((cur1` M)` y):ran M-1-1-onto->ran M)
138122, 123, 136, 137syl111anc 1100 . . . . . . . . . . . . . . . . . . . . . 22 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` y):ran M-1-1-onto->ran M)
139 fvex 4689 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((cur1` M)` y) e. _V
140 f1oeq1 4630 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = ((cur1` M)` y) -> (z:ran M-1-1-onto->ran M <-> ((cur1` M)` y):ran M-1-1-onto->ran M))
141140elabg 2405 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((cur1` M)` y) e. _V -> (((cur1` M)` y) e. {z | z:ran M-1-1-onto->ran M} <-> ((cur1` M)` y):ran M-1-1-onto->ran M))
142139, 141ax-mp 7 . . . . . . . . . . . . . . . . . . . . . 22 |- (((cur1` M)` y) e. {z | z:ran M-1-1-onto->ran M} <-> ((cur1` M)` y):ran M-1-1-onto->ran M)
143138, 142sylibr 217 . . . . . . . . . . . . . . . . . . . . 21 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((cur1` M)` y) e. {z | z:ran M-1-1-onto->ran M})
144143adantl 424 . . . . . . . . . . . . . . . . . . . 20 |- ((((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> ((cur1` M)` y) e. {z | z:ran M-1-1-onto->ran M})
145135, 144eqeltrrd 1972 . . . . . . . . . . . . . . . . . . 19 |- ((((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M})
146145adantll 428 . . . . . . . . . . . . . . . . . 18 |- (((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))}) /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M})
147134, 146jca 310 . . . . . . . . . . . . . . . . 17 |- (((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))}) /\ ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G))) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M} /\ {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M}))
148147ex 402 . . . . . . . . . . . . . . . 16 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))}) -> (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M} /\ {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M})))
1491483adant3 896 . . . . . . . . . . . . . . 15 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))}) -> (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M} /\ {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M})))
150149impcom 378 . . . . . . . . . . . . . 14 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M} /\ {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M}))
151 eqid 1884 . . . . . . . . . . . . . . 15 |- {z | z:ran M-1-1-onto->ran M} = {z | z:ran M-1-1-onto->ran M}
1529, 151symgoprv 10203 . . . . . . . . . . . . . 14 |- (({<.a, b>. | (a e. ran M /\ b = (xMa))} e. {z | z:ran M-1-1-onto->ran M} /\ {<.m, n>. | (m e. ran M /\ n = (yMm))} e. {z | z:ran M-1-1-onto->ran M}) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}) = ({<.a, b>. | (a e. ran M /\ b = (xMa))} o. {<.m, n>. | (m e. ran M /\ n = (yMm))}))
153150, 152syl 12 . . . . . . . . . . . . 13 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}) = ({<.a, b>. | (a e. ran M /\ b = (xMa))} o. {<.m, n>. | (m e. ran M /\ n = (yMm))}))
154 foprrn 4965 . . . . . . . . . . . . . . . . . . . . . 22 |- ((M:(ran G X. ran M)-->ran M /\ y e. ran G /\ m e. ran M) -> (yMm) e. ran M)
1551543exp 1066 . . . . . . . . . . . . . . . . . . . . 21 |- (M:(ran G X. ran M)-->ran M -> (y e. ran G -> (m e. ran M -> (yMm) e. ran M)))
1561553ad2ant2 898 . . . . . . . . . . . . . . . . . . . 20 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (y e. ran G -> (m e. ran M -> (yMm) e. ran M)))
157156com12 14 . . . . . . . . . . . . . . . . . . 19 |- (y e. ran G -> ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (m e. ran M -> (yMm) e. ran M)))
158157adantl 424 . . . . . . . . . . . . . . . . . 18 |- ((x e. ran G /\ y e. ran G) -> ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (m e. ran M -> (yMm) e. ran M)))
159158imp 377 . . . . . . . . . . . . . . . . 17 |- (((x e. ran G /\ y e. ran G) /\ (G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))) -> (m e. ran M -> (yMm) e. ran M))
160159r19.21aiv 2175 . . . . . . . . . . . . . . . 16 |- (((x e. ran G /\ y e. ran G) /\ (G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))))) -> A.m e. ran M(yMm) e. ran M)
161160ancoms 484 . . . . . . . . . . . . . . 15 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> A.m e. ran M(yMm) e. ran M)
162161adantr 425 . . . . . . . . . . . . . 14 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> A.m e. ran M(yMm) e. ran M)
163 oprex 4907 . . . . . . . . . . . . . . . . . . 19 |- (xMa) e. _V
164163a1i 8 . . . . . . . . . . . . . . . . . 18 |- (a e. ran M -> (xMa) e. _V)
165164rgen 2159 . . . . . . . . . . . . . . . . 17 |- A.a e. ran M(xMa) e. _V
166165a1i 8 . . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> A.a e. ran M(xMa) e. _V)
167 eqid 1884 . . . . . . . . . . . . . . . . 17 |- {<.a, b>. | (a e. ran M /\ b = (xMa))} = {<.a, b>. | (a e. ran M /\ b = (xMa))}
168167fnopab2g 4547 . . . . . . . . . . . . . . . 16 |- (A.a e. ran M(xMa) e. _V <-> {<.a, b>. | (a e. ran M /\ b = (xMa))} Fn ran M)
169166, 168sylib 215 . . . . . . . . . . . . . . 15 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> {<.a, b>. | (a e. ran M /\ b = (xMa))} Fn ran M)
170169adantr 425 . . . . . . . . . . . . . 14 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> {<.a, b>. | (a e. ran M /\ b = (xMa))} Fn ran M)
171 eqid 1884 . . . . . . . . . . . . . . . 16 |- {<.m, n>. | (m e. ran M /\ n = (yMm))} = {<.m, n>. | (m e. ran M /\ n = (yMm))}
172 eqid 1884 . . . . . . . . . . . . . . . 16 |- {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))} = {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))}
173171, 172fnopabco2b 14734 . . . . . . . . . . . . . . 15 |- ((A.m e. ran M(yMm) e. ran M /\ {<.a, b>. | (a e. ran M /\ b = (xMa))} Fn ran M) -> {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))} = ({<.a, b>. | (a e. ran M /\ b = (xMa))} o. {<.m, n>. | (m e. ran M /\ n = (yMm))}))
174173eqcomd 1889 . . . . . . . . . . . . . 14 |- ((A.m e. ran M(yMm) e. ran M /\ {<.a, b>. | (a e. ran M /\ b = (xMa))} Fn ran M) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} o. {<.m, n>. | (m e. ran M /\ n = (yMm))}) = {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))})
175162, 170, 174syl11anc 524 . . . . . . . . . . . . 13 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} o. {<.m, n>. | (m e. ran M /\ n = (yMm))}) = {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))})
176 opreq2 4890 . . . . . . . . . . . . . . . . . . . 20 |- (a = (yMm) -> (xMa) = (xM(yMm)))
177176, 167fvopab4g 4742 . . . . . . . . . . . . . . . . . . 19 |- (((yMm) e. ran M /\ (xM(yMm)) e. _V) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)) = (xM(yMm)))
178158impcom 378 . . . . . . . . . . . . . . . . . . . 20 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (m e. ran M -> (yMm) e. ran M))
179178imp 377 . . . . . . . . . . . . . . . . . . 19 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ m e. ran M) -> (yMm) e. ran M)
180 oprex 4907 . . . . . . . . . . . . . . . . . . 19 |- (xM(yMm)) e. _V
181177, 179, 180sylancl 525 . . . . . . . . . . . . . . . . . 18 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ m e. ran M) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)) = (xM(yMm)))
182 opreq2 4890 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (f = m -> ((Id` G)Mf) = ((Id` G)Mm))
183 id 73 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (f = m -> f = m)
184182, 183eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . 23 |- (f = m -> (((Id` G)Mf) = f <-> ((Id` G)Mm) = m))
185 opreq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = m -> ((xGy)Mf) = ((xGy)Mm))
186 opreq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f = m -> (yMf) = (yMm))
187186opreq2d 4898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = m -> (xM(yMf)) = (xM(yMm)))
188185, 187eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f = m -> (((xGy)Mf) = (xM(yMf)) <-> ((xGy)Mm) = (xM(yMm))))
189188ralbidv 2123 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (f = m -> (A.y e. ran G((xGy)Mf) = (xM(yMf)) <-> A.y e. ran G((xGy)Mm) = (xM(yMm))))
190189ralbidv 2123 . . . . . . . . . . . . . . . . . . . . . . 23 |- (f = m -> (A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)) <-> A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))))
191184, 190anbi12d 690 . . . . . . . . . . . . . . . . . . . . . 22 |- (f = m -> ((((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) <-> (((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)))))
192191cbvralv 2280 . . . . . . . . . . . . . . . . . . . . 21 |- (A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) <-> A.m e. ran M(((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))))
193 ra4 2155 . . . . . . . . . . . . . . . . . . . . . . 23 |- (A.m e. ran M(((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))) -> (m e. ran M -> (((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)))))
194 ra42 2157 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)) -> ((x e. ran G /\ y e. ran G) -> ((xGy)Mm) = (xM(yMm))))
195194imp 377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)) /\ (x e. ran G /\ y e. ran G)) -> ((xGy)Mm) = (xM(yMm)))
196195eqcomd 1889 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)) /\ (x e. ran G /\ y e. ran G)) -> (xM(yMm)) = ((xGy)Mm))
197196ex 402 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm)) -> ((x e. ran G /\ y e. ran G) -> (xM(yMm)) = ((xGy)Mm)))
198197adantl 424 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))) -> ((x e. ran G /\ y e. ran G) -> (xM(yMm)) = ((xGy)Mm)))
199193, 198syl6 25 . . . . . . . . . . . . . . . . . . . . . 22 |- (A.m e. ran M(((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))) -> (m e. ran M -> ((x e. ran G /\ y e. ran G) -> (xM(yMm)) = ((xGy)Mm))))
200199com23 36 . . . . . . . . . . . . . . . . . . . . 21 |- (A.m e. ran M(((Id` G)Mm) = m /\ A.x e. ran GA.y e. ran G((xGy)Mm) = (xM(yMm))) -> ((x e. ran G /\ y e. ran G) -> (m e. ran M -> (xM(yMm)) = ((xGy)Mm))))
201192, 200sylbi 216 . . . . . . . . . . . . . . . . . . . 20 |- (A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf))) -> ((x e. ran G /\ y e. ran G) -> (m e. ran M -> (xM(yMm)) = ((xGy)Mm))))
2022013ad2ant3 899 . . . . . . . . . . . . . . . . . . 19 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((x e. ran G /\ y e. ran G) -> (m e. ran M -> (xM(yMm)) = ((xGy)Mm))))
203202imp31 389 . . . . . . . . . . . . . . . . . 18 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ m e. ran M) -> (xM(yMm)) = ((xGy)Mm))
204181, 203eqtrd 1925 . . . . . . . . . . . . . . . . 17 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ m e. ran M) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)) = ((xGy)Mm))
205204eqeq2d 1895 . . . . . . . . . . . . . . . 16 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ m e. ran M) -> (n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)) <-> n = ((xGy)Mm)))
206205pm5.32da 711 . . . . . . . . . . . . . . 15 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> ((m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm))) <-> (m e. ran M /\ n = ((xGy)Mm))))
207206opabbidv 3401 . . . . . . . . . . . . . 14 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))} = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})
208207adantr 425 . . . . . . . . . . . . 13 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> {<.m, n>. | (m e. ran M /\ n = ({<.a, b>. | (a e. ran M /\ b = (xMa))}` (yMm)))} = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})
209153, 175, 2083eqtrd 1929 . . . . . . . . . . . 12 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> ({<.a, b>. | (a e. ran M /\ b = (xMa))} (SymGrp` ran M){<.m, n>. | (m e. ran M /\ n = (yMm))}) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})
210 eqcom 1886 . . . . . . . . . . . . . . 15 |- (((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} <-> {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} = ((cur1` M)` (xGy)))
211210biimpi 168 . . . . . . . . . . . . . 14 |- (((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} -> {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} = ((cur1` M)` (xGy)))
2122113ad2ant3 899 . . . . . . . . . . . . 13 |- ((((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))}) -> {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} = ((cur1` M)` (xGy)))
213212adantl 424 . . . . . . . . . . . 12 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))} = ((cur1` M)` (xGy)))
214120, 209, 2133eqtrd 1929 . . . . . . . . . . 11 |- ((((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) /\ (((cur1` M)` x) = {<.a, b>. | (a e. ran M /\ b = (xMa))} /\ ((cur1` M)` y) = {<.m, n>. | (m e. ran M /\ n = (yMm))} /\ ((cur1` M)` (xGy)) = {<.m, n>. | (m e. ran M /\ n = ((xGy)Mm))})) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))
215117, 214mpdan 768 . . . . . . . . . 10 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ (x e. ran G /\ y e. ran G)) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))
216215ex 402 . . . . . . . . 9 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((x e. ran G /\ y e. ran G) -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy))))
217216expdimp 406 . . . . . . . 8 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ x e. ran G) -> (y e. ran G -> (((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy))))
218102, 217r19.21ai 2174 . . . . . . 7 |- (((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) /\ x e. ran G) -> A.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))
219218ex 402 . . . . . 6 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (x e. ran G -> A.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy))))
22049, 219r19.21ai 2174 . . . . 5 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> A.x e. ran GA.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))
221101, 220jca 310 . . . 4 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((cur1` M):ran G-->{f | f:ran M-1-1-onto->ran M} /\ A.x e. ran GA.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy))))
22279rnex 4209 . . . . . . . 8 |- ran M e. _V
223 eqid 1884 . . . . . . . 8 |- {f | f:ran M-1-1-onto->ran M} = {f | f:ran M-1-1-onto->ran M}
224222, 223symgfo 14730 . . . . . . 7 |- (SymGrp` ran M):({f | f:ran M-1-1-onto->ran M} X. {f | f:ran M-1-1-onto->ran M})-onto->{f | f:ran M-1-1-onto->ran M}
225 forn 4620 . . . . . . . 8 |- ((SymGrp` ran M):({f | f:ran M-1-1-onto->ran M} X. {f | f:ran M-1-1-onto->ran M})-onto->{f | f:ran M-1-1-onto->ran M} -> ran (SymGrp` ran M) = {f | f:ran M-1-1-onto->ran M})
226225eqcomd 1889 . . . . . . 7 |- ((SymGrp` ran M):({f | f:ran M-1-1-onto->ran M} X. {f | f:ran M-1-1-onto->ran M})-onto->{f | f:ran M-1-1-onto->ran M} -> {f | f:ran M-1-1-onto->ran M} = ran (SymGrp` ran M))
227224, 226ax-mp 7 . . . . . 6 |- {f | f:ran M-1-1-onto->ran M} = ran (SymGrp` ran M)
2282, 227elghom 10195 . . . . 5 |- ((G e. Grp /\ (SymGrp` ran M) e. Grp) -> ((cur1` M) e. (G GrpHom (SymGrp` ran M)) <-> ((cur1` M):ran G-->{f | f:ran M-1-1-onto->ran M} /\ A.x e. ran GA.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))))
229 simp1 876 . . . . 5 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> G e. Grp)
230222symggrpi 10205 . . . . 5 |- (SymGrp` ran M) e. Grp
231228, 229, 230sylancl 525 . . . 4 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> ((cur1` M) e. (G GrpHom (SymGrp` ran M)) <-> ((cur1` M):ran G-->{f | f:ran M-1-1-onto->ran M} /\ A.x e. ran GA.y e. ran G(((cur1` M)` x)(SymGrp` ran M)((cur1` M)` y)) = ((cur1` M)` (xGy)))))
232221, 231mpbird 213 . . 3 |- ((G e. Grp /\ M:(ran G X. ran M)-->ran M /\ A.f e. ran M(((Id` G)Mf) = f /\ A.x e. ran GA.y e. ran G((xGy)Mf) = (xM(yMf)))) -> (cur1` M) e. (G GrpHom (SymGrp` ran M)))
2335, 232syl6bi 231 . 2 |- (M e. A -> (<.G, M>. e. GrpAct -> (cur1` M) e. (G GrpHom (SymGrp` ran M))))
2341, 233ax-mp 7 1 |- (<.G, M>. e. GrpAct -> (cur1` M) e. (G GrpHom (SymGrp` ran M)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  _Vcvv 2292  (/)c0 2875  <.cop 3046  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312  GrpActcga 9447   GrpHom cghom 10189  SymGrpcsymgrp 10198  cur1ccur1 14542
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  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-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-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-ginv 9318  df-ga 9448  df-ghom 10190  df-symgrp 10199  df-exid 10362  df-mgm 10366  df-cur1 14544
Copyright terms: Public domain