symggrpi - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem symggrpi 10340

Description: The symmetry group on A is a group (inference version). (Contributed by Paul Chapman, 25-Feb-2008.)

**Hypothesis**
Ref	Expression
symggrpi.1	⊢ A ∈ V

**Assertion**
Ref	Expression
symggrpi	⊢ (SymGrp ‘A) ∈ Grp

**Proof of Theorem symggrpi**
Step	Hyp	Ref	Expression
1		symggrpi.1	. . 3 ⊢ A ∈ V
2		eqid 1473	. . . . 5 ⊢ {x∣x:A–1-1-onto→A} = {x∣x:A–1-1-onto→A}
3		equid 1124	. . . . . . 7 ⊢ x = x
4	3	biantru 723	. . . . . 6 ⊢ (x:A–1-1-onto→A ↔ (x:A–1-1-onto→A ⋀ x = x))
5	4	abbii 1572	. . . . 5 ⊢ {x∣x:A–1-1-onto→A} = {x∣(x:A–1-1-onto→A ⋀ x = x)}
6	2, 5	eqtr 1492	. . . 4 ⊢ {x∣x:A–1-1-onto→A} = {x∣(x:A–1-1-onto→A ⋀ x = x)}
7	6	f1oabexg 3691	. . 3 ⊢ ((A ∈ V ⋀ A ∈ V) → {x∣x:A–1-1-onto→A} ∈ V)
8	1, 1, 7	mp2an 696	. 2 ⊢ {x∣x:A–1-1-onto→A} ∈ V
9	1, 2	symgf 10339	. 2 ⊢ (SymGrp ‘A):({x∣x:A–1-1-onto→A} × {x∣x:A–1-1-onto→A})–→{x∣x:A–1-1-onto→A}
10		coass 3504	. . 3 ⊢ ((f ∘ g) ∘ h) = (f ∘ (g ∘ h))
11	1, 2	symgoprval 10338	. . . . . 6 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)g) = (f ∘ g))
12	11	3adant3 798	. . . . 5 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)g) = (f ∘ g))
13	12	opreq1d 3966	. . . 4 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f(SymGrp ‘A)g)(SymGrp ‘A)h) = ((f ∘ g)(SymGrp ‘A)h))
14	1, 2	symgoprval 10338	. . . . . 6 ⊢ (((f ∘ g) ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f ∘ g)(SymGrp ‘A)h) = ((f ∘ g) ∘ h))
15		f1oco 3698	. . . . . . 7 ⊢ ((f:A–1-1-onto→A ⋀ g:A–1-1-onto→A) → (f ∘ g):A–1-1-onto→A)
16	1, 2	elsymgrn 10335	. . . . . . . 8 ⊢ (f ∈ {x∣x:A–1-1-onto→A} ↔ f:A–1-1-onto→A)
17	1, 2	elsymgrn 10335	. . . . . . . 8 ⊢ (g ∈ {x∣x:A–1-1-onto→A} ↔ g:A–1-1-onto→A)
18	16, 17	anbi12i 482	. . . . . . 7 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A}) ↔ (f:A–1-1-onto→A ⋀ g:A–1-1-onto→A))
19	1, 2	elsymgrn 10335	. . . . . . 7 ⊢ ((f ∘ g) ∈ {x∣x:A–1-1-onto→A} ↔ (f ∘ g):A–1-1-onto→A)
20	15, 18, 19	3imtr4 219	. . . . . 6 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A}) → (f ∘ g) ∈ {x∣x:A–1-1-onto→A})
21	14, 20	sylan 448	. . . . 5 ⊢ (((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A}) ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f ∘ g)(SymGrp ‘A)h) = ((f ∘ g) ∘ h))
22	21	3impa 827	. . . 4 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f ∘ g)(SymGrp ‘A)h) = ((f ∘ g) ∘ h))
23	13, 22	eqtrd 1504	. . 3 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f(SymGrp ‘A)g)(SymGrp ‘A)h) = ((f ∘ g) ∘ h))
24	1, 2	symgoprval 10338	. . . . . 6 ⊢ ((g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (g(SymGrp ‘A)h) = (g ∘ h))
25	24	3adant1 796	. . . . 5 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (g(SymGrp ‘A)h) = (g ∘ h))
26	25	opreq2d 3967	. . . 4 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)(g(SymGrp ‘A)h)) = (f(SymGrp ‘A)(g ∘ h)))
27	1, 2	symgoprval 10338	. . . . . 6 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ (g ∘ h) ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)(g ∘ h)) = (f ∘ (g ∘ h)))
28		f1oco 3698	. . . . . . 7 ⊢ ((g:A–1-1-onto→A ⋀ h:A–1-1-onto→A) → (g ∘ h):A–1-1-onto→A)
29	1, 2	elsymgrn 10335	. . . . . . . 8 ⊢ (h ∈ {x∣x:A–1-1-onto→A} ↔ h:A–1-1-onto→A)
30	17, 29	anbi12i 482	. . . . . . 7 ⊢ ((g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) ↔ (g:A–1-1-onto→A ⋀ h:A–1-1-onto→A))
31	1, 2	elsymgrn 10335	. . . . . . 7 ⊢ ((g ∘ h) ∈ {x∣x:A–1-1-onto→A} ↔ (g ∘ h):A–1-1-onto→A)
32	28, 30, 31	3imtr4 219	. . . . . 6 ⊢ ((g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (g ∘ h) ∈ {x∣x:A–1-1-onto→A})
33	27, 32	sylan2 451	. . . . 5 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ (g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A})) → (f(SymGrp ‘A)(g ∘ h)) = (f ∘ (g ∘ h)))
34	33	3impb 828	. . . 4 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)(g ∘ h)) = (f ∘ (g ∘ h)))
35	26, 34	eqtrd 1504	. . 3 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → (f(SymGrp ‘A)(g(SymGrp ‘A)h)) = (f ∘ (g ∘ h)))
36	10, 23, 35	3eqtr4a 1529	. 2 ⊢ ((f ∈ {x∣x:A–1-1-onto→A} ⋀ g ∈ {x∣x:A–1-1-onto→A} ⋀ h ∈ {x∣x:A–1-1-onto→A}) → ((f(SymGrp ‘A)g)(SymGrp ‘A)h) = (f(SymGrp ‘A)(g(SymGrp ‘A)h)))
37		f1oi 3708	. . 3 ⊢ (I ↾ A):A–1-1-onto→A
38	1, 2	elsymgrn 10335	. . 3 ⊢ ((I ↾ A) ∈ {x∣x:A–1-1-onto→A} ↔ (I ↾ A):A–1-1-onto→A)
39	37, 38	mpbir 190	. 2 ⊢ (I ↾ A) ∈ {x∣x:A–1-1-onto→A}
40	1, 2	symgoprval 10338	. . . 4 ⊢ (((I ↾ A) ∈ {x∣x:A–1-1-onto→A} ⋀ f ∈ {x∣x:A–1-1-onto→A}) → ((I ↾ A)(SymGrp ‘A)f) = ((I ↾ A) ∘ f))
41	39, 40	mpan 694	. . 3 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → ((I ↾ A)(SymGrp ‘A)f) = ((I ↾ A) ∘ f))
42		f1of 3680	. . . . 5 ⊢ (f:A–1-1-onto→A → f:A–→A)
43		fcoi2 3637	. . . . 5 ⊢ (f:A–→A → ((I ↾ A) ∘ f) = f)
44	42, 43	syl 10	. . . 4 ⊢ (f:A–1-1-onto→A → ((I ↾ A) ∘ f) = f)
45	16, 44	sylbi 199	. . 3 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → ((I ↾ A) ∘ f) = f)
46	41, 45	eqtrd 1504	. 2 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → ((I ↾ A)(SymGrp ‘A)f) = f)
47		f1ocnv 3692	. . 3 ⊢ (f:A–1-1-onto→A → ^◡f:A–1-1-onto→A)
48	1, 2	elsymgrn 10335	. . 3 ⊢ (^◡f ∈ {x∣x:A–1-1-onto→A} ↔ ^◡f:A–1-1-onto→A)
49	47, 16, 48	3imtr4 219	. 2 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → ^◡f ∈ {x∣x:A–1-1-onto→A})
50	1, 2	symgoprval 10338	. . . 4 ⊢ ((^◡f ∈ {x∣x:A–1-1-onto→A} ⋀ f ∈ {x∣x:A–1-1-onto→A}) → (^◡f(SymGrp ‘A)f) = (^◡f ∘ f))
51	49, 50	mpancom 704	. . 3 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → (^◡f(SymGrp ‘A)f) = (^◡f ∘ f))
52		f1ococnv1 3700	. . . 4 ⊢ (f:A–1-1-onto→A → (^◡f ∘ f) = (I ↾ A))
53	16, 52	sylbi 199	. . 3 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → (^◡f ∘ f) = (I ↾ A))
54	51, 53	eqtrd 1504	. 2 ⊢ (f ∈ {x∣x:A–1-1-onto→A} → (^◡f(SymGrp ‘A)f) = (I ↾ A))
55	8, 9, 36, 39, 46, 49, 54	isgrpi 7992	1 ⊢ (SymGrp ‘A) ∈ Grp

Colors of variables: wff set class

Syntax hints: ⋀ wa 223 ⋀ w3a 774 = wceq 954 ∈ wcel 956 {cab 1461 Vcvv 1807 Icid 2826 ^◡ccnv 3164 ↾ cres 3167 ∘ ccom 3169 –→wf 3173 –1-1-onto→wf1o 3176 ‘cfv 3177 (class class class)co 3954 Grpcgr 7983 SymGrpcsymgrp 10333

This theorem is referenced by: symgidi 10341 symggrp 10342 cayleylem2 10344 cayleylem3 10345

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-nul 2277 df-pw 2398 df-sn 2408 df-pr 2409 df-op 2412 df-uni 2499 df-br 2615 df-opab 2662 df-id 2830 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-fv 3193 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-grp 7987 df-symgrp 10334