HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem symggrpi 10313
Description: The symmetry group on A is a group (inference version). (Contributed by Paul Chapman, 25-Feb-2008.)
Hypothesis
Ref Expression
symggrpi.1 |- A e. V
Assertion
Ref Expression
symggrpi |- (SymGrp` A) e. Grp
Proof of Theorem symggrpi
StepHypRef Expression
1 symggrpi.1 . . 3 |- A e. V
2 eqid 1468 . . . . 5 |- {x | x:A-1-1-onto->A} = {x | x:A-1-1-onto->A}
3 equid 1122 . . . . . . 7 |- x = x
43biantru 722 . . . . . 6 |- (x:A-1-1-onto->A <-> (x:A-1-1-onto->A /\ x = x))
54abbii 1567 . . . . 5 |- {x | x:A-1-1-onto->A} = {x | (x:A-1-1-onto->A /\ x = x)}
62, 5eqtr 1487 . . . 4 |- {x | x:A-1-1-onto->A} = {x | (x:A-1-1-onto->A /\ x = x)}
76f1oabexg 3685 . . 3 |- ((A e. V /\ A e. V) -> {x | x:A-1-1-onto->A} e. V)
81, 1, 7mp2an 695 . 2 |- {x | x:A-1-1-onto->A} e. V
91, 2symgf 10310 . 2 |- (SymGrp` A):({x | x:A-1-1-onto->A} X. {x | x:A-1-1-onto->A})-->{x | x:A-1-1-onto->A}
10 coass 3498 . . 3 |- ((f o. g) o. h) = (f o. (g o. h))
111, 2symgoprval 10309 . . . . . 6 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)g) = (f o. g))
12113adant3 797 . . . . 5 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)g) = (f o. g))
1312opreq1d 3960 . . . 4 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> ((f(SymGrp` A)g)(SymGrp` A)h) = ((f o. g)(SymGrp` A)h))
141, 2symgoprval 10309 . . . . . 6 |- (((f o. g) e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> ((f o. g)(SymGrp` A)h) = ((f o. g) o. h))
15 f1oco 3692 . . . . . . 7 |- ((f:A-1-1-onto->A /\ g:A-1-1-onto->A) -> (f o. g):A-1-1-onto->A)
161, 2elsymgrn 10306 . . . . . . . 8 |- (f e. {x | x:A-1-1-onto->A} <-> f:A-1-1-onto->A)
171, 2elsymgrn 10306 . . . . . . . 8 |- (g e. {x | x:A-1-1-onto->A} <-> g:A-1-1-onto->A)
1816, 17anbi12i 481 . . . . . . 7 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A}) <-> (f:A-1-1-onto->A /\ g:A-1-1-onto->A))
191, 2elsymgrn 10306 . . . . . . 7 |- ((f o. g) e. {x | x:A-1-1-onto->A} <-> (f o. g):A-1-1-onto->A)
2015, 18, 193imtr4 219 . . . . . 6 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A}) -> (f o. g) e. {x | x:A-1-1-onto->A})
2114, 20sylan 448 . . . . 5 |- (((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A}) /\ h e. {x | x:A-1-1-onto->A}) -> ((f o. g)(SymGrp` A)h) = ((f o. g) o. h))
22213impa 826 . . . 4 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> ((f o. g)(SymGrp` A)h) = ((f o. g) o. h))
2313, 22eqtrd 1499 . . 3 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> ((f(SymGrp` A)g)(SymGrp` A)h) = ((f o. g) o. h))
241, 2symgoprval 10309 . . . . . 6 |- ((g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (g(SymGrp` A)h) = (g o. h))
25243adant1 795 . . . . 5 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (g(SymGrp` A)h) = (g o. h))
2625opreq2d 3961 . . . 4 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)(g(SymGrp` A)h)) = (f(SymGrp` A)(g o. h)))
271, 2symgoprval 10309 . . . . . 6 |- ((f e. {x | x:A-1-1-onto->A} /\ (g o. h) e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)(g o. h)) = (f o. (g o. h)))
28 f1oco 3692 . . . . . . 7 |- ((g:A-1-1-onto->A /\ h:A-1-1-onto->A) -> (g o. h):A-1-1-onto->A)
291, 2elsymgrn 10306 . . . . . . . 8 |- (h e. {x | x:A-1-1-onto->A} <-> h:A-1-1-onto->A)
3017, 29anbi12i 481 . . . . . . 7 |- ((g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) <-> (g:A-1-1-onto->A /\ h:A-1-1-onto->A))
311, 2elsymgrn 10306 . . . . . . 7 |- ((g o. h) e. {x | x:A-1-1-onto->A} <-> (g o. h):A-1-1-onto->A)
3228, 30, 313imtr4 219 . . . . . 6 |- ((g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (g o. h) e. {x | x:A-1-1-onto->A})
3327, 32sylan2 451 . . . . 5 |- ((f e. {x | x:A-1-1-onto->A} /\ (g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A})) -> (f(SymGrp` A)(g o. h)) = (f o. (g o. h)))
34333impb 827 . . . 4 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)(g o. h)) = (f o. (g o. h)))
3526, 34eqtrd 1499 . . 3 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> (f(SymGrp` A)(g(SymGrp` A)h)) = (f o. (g o. h)))
3610, 23, 353eqtr4a 1524 . 2 |- ((f e. {x | x:A-1-1-onto->A} /\ g e. {x | x:A-1-1-onto->A} /\ h e. {x | x:A-1-1-onto->A}) -> ((f(SymGrp` A)g)(SymGrp` A)h) = (f(SymGrp` A)(g(SymGrp` A)h)))
37 f1oi 3702 . . 3 |- (I |` A):A-1-1-onto->A
381, 2elsymgrn 10306 . . 3 |- ((I |` A) e. {x | x:A-1-1-onto->A} <-> (I |` A):A-1-1-onto->A)
3937, 38mpbir 190 . 2 |- (I |` A) e. {x | x:A-1-1-onto->A}
401, 2symgoprval 10309 . . . 4 |- (((I |` A) e. {x | x:A-1-1-onto->A} /\ f e. {x | x:A-1-1-onto->A}) -> ((I |` A)(SymGrp` A)f) = ((I |` A) o. f))
4139, 40mpan 693 . . 3 |- (f e. {x | x:A-1-1-onto->A} -> ((I |` A)(SymGrp` A)f) = ((I |` A) o. f))
42 f1of 3674 . . . . 5 |- (f:A-1-1-onto->A -> f:A-->A)
43 fcoi2 3631 . . . . 5 |- (f:A-->A -> ((I |` A) o. f) = f)
4442, 43syl 10 . . . 4 |- (f:A-1-1-onto->A -> ((I |` A) o. f) = f)
4516, 44sylbi 199 . . 3 |- (f e. {x | x:A-1-1-onto->A} -> ((I |` A) o. f) = f)
4641, 45eqtrd 1499 . 2 |- (f e. {x | x:A-1-1-onto->A} -> ((I |` A)(SymGrp` A)f) = f)
47 f1ocnv 3686 . . 3 |- (f:A-1-1-onto->A -> `'f:A-1-1-onto->A)
481, 2elsymgrn 10306 . . 3 |- (`'f e. {x | x:A-1-1-onto->A} <-> `'f:A-1-1-onto->A)
4947, 16, 483imtr4 219 . 2 |- (f e. {x | x:A-1-1-onto->A} -> `'f e. {x | x:A-1-1-onto->A})
501, 2symgoprval 10309 . . . 4 |- ((`'f e. {x | x:A-1-1-onto->A} /\ f e. {x | x:A-1-1-onto->A}) -> (`'f(SymGrp` A)f) = (`'f o. f))
5149, 50mpancom 703 . . 3 |- (f e. {x | x:A-1-1-onto->A} -> (`'f(SymGrp` A)f) = (`'f o. f))
52 f1ococnv1 3694 . . . 4 |- (f:A-1-1-onto->A -> (`'f o. f) = (I |` A))
5316, 52sylbi 199 . . 3 |- (f e. {x | x:A-1-1-onto->A} -> (`'f o. f) = (I |` A))
5451, 53eqtrd 1499 . 2 |- (f e. {x | x:A-1-1-onto->A} -> (`'f(SymGrp` A)f) = (I |` A))
558, 9, 36, 39, 46, 49, 54isgrpi 7976 1 |- (SymGrp` A) e. Grp
Colors of variables: wff set class
Syntax hints:   /\ wa 223   /\ w3a 773   = wceq 953   e. wcel 955  {cab 1456  Vcvv 1802  Icid 2820  `'ccnv 3159   |` cres 3162   o. ccom 3164  -->wf 3168  -1-1-onto->wf1o 3171  ` cfv 3172  (class class class)co 3948  Grpcgr 7967  SymGrpcsymgrp 10304
This theorem is referenced by:  symgidi 10314  symggrp 10315  cayleylem2 10317  cayleylem3 10318
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6