Theorem isga 18812

Description: The predicate "is a (left) group action". The group 𝐺 is said to act on the base set 𝑌 of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element 𝑔 of 𝐺 is a permutation of the elements of 𝑌 (see gapm 18827). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)

Hypotheses

Ref	Expression
isga.1	⊢ 𝑋 = (Base‘𝐺)
isga.2	⊢ + = (+g‘𝐺)
isga.3	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
isga	⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐺   𝑦,𝑋,𝑧   𝑥,𝑌,𝑦,𝑧   𝑥, ⊕ ,𝑦,𝑧

Allowed substitution hints:   + (𝑥,𝑦,𝑧)   𝑋(𝑥)   0 (𝑥,𝑦,𝑧)

Proof of Theorem isga

Dummy variables 𝑔 𝑏 𝑚 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ga 18811	. . 3 ⊢ GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
2	1	elmpocl 7489	. 2 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V))
3		fvexd 6771	. . . . . . 7 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) ∈ V)
4		simplr 765	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌)
5		id 22	. . . . . . . . . . 11 ⊢ (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔))
6		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → 𝑔 = 𝐺)
7	6	fveq2d 6760	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺))
8		isga.1	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝐺)
9	7, 8	eqtr4di 2797	. . . . . . . . . . 11 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = 𝑋)
10	5, 9	sylan9eqr 2801	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋)
11	10, 4	xpeq12d 5611	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌))
12	4, 11	oveq12d 7273	. . . . . . . 8 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠 ↑m (𝑏 × 𝑠)) = (𝑌 ↑m (𝑋 × 𝑌)))
13		simpll 763	. . . . . . . . . . . . . 14 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺)
14	13	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = (0g‘𝐺))
15		isga.3	. . . . . . . . . . . . 13 ⊢ 0 = (0g‘𝐺)
16	14, 15	eqtr4di 2797	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = 0 )
17	16	oveq1d 7270	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g‘𝑔)𝑚𝑥) = ( 0 𝑚𝑥))
18	17	eqeq1d 2740	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g‘𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥))
19	13	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = (+g‘𝐺))
20		isga.2	. . . . . . . . . . . . . . . 16 ⊢ + = (+g‘𝐺)
21	19, 20	eqtr4di 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = + )
22	21	oveqd 7272	. . . . . . . . . . . . . 14 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g‘𝑔)𝑧) = (𝑦 + 𝑧))
23	22	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥))
24	23	eqeq1d 2740	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
25	10, 24	raleqbidv 3327	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
26	10, 25	raleqbidv 3327	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
27	18, 26	anbi12d 630	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
28	4, 27	raleqbidv 3327	. . . . . . . 8 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
29	12, 28	rabeqbidv 3410	. . . . . . 7 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
30	3, 29	csbied 3866	. . . . . 6 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
31		ovex 7288	. . . . . . 7 ⊢ (𝑌 ↑m (𝑋 × 𝑌)) ∈ V
32	31	rabex 5251	. . . . . 6 ⊢ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V
33	30, 1, 32	ovmpoa 7406	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
34	33	eleq2d 2824	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ⊕ ∈ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}))
35		oveq 7261	. . . . . . . 8 ⊢ (𝑚 = ⊕ → ( 0 𝑚𝑥) = ( 0 ⊕ 𝑥))
36	35	eqeq1d 2740	. . . . . . 7 ⊢ (𝑚 = ⊕ → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 ⊕ 𝑥) = 𝑥))
37		oveq 7261	. . . . . . . . 9 ⊢ (𝑚 = ⊕ → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) ⊕ 𝑥))
38		oveq 7261	. . . . . . . . . 10 ⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧𝑚𝑥)))
39		oveq 7261	. . . . . . . . . . 11 ⊢ (𝑚 = ⊕ → (𝑧𝑚𝑥) = (𝑧 ⊕ 𝑥))
40	39	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑚 = ⊕ → (𝑦 ⊕ (𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))
41	38, 40	eqtrd 2778	. . . . . . . . 9 ⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))
42	37, 41	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑚 = ⊕ → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))
43	42	2ralbidv 3122	. . . . . . 7 ⊢ (𝑚 = ⊕ → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))
44	36, 43	anbi12d 630	. . . . . 6 ⊢ (𝑚 = ⊕ → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
45	44	ralbidv 3120	. . . . 5 ⊢ (𝑚 = ⊕ → (∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
46	45	elrab 3617	. . . 4 ⊢ ( ⊕ ∈ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
47	34, 46	bitrdi 286	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
48		simpr 484	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V)
49	8	fvexi 6770	. . . . . 6 ⊢ 𝑋 ∈ V
50		xpexg 7578	. . . . . 6 ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
51	49, 48, 50	sylancr 586	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
52	48, 51	elmapd 8587	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌))
53	52	anbi1d 629	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
54	47, 53	bitrd 278	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
55	2, 54	biadanii 818	1 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  {crab 3067  Vcvv 3422  ⦋csb 3828   × cxp 5578  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255   ↑_m cmap 8573  Basecbs 16840  +_gcplusg 16888  0_gc0g 17067  Grpcgrp 18492   GrpAct cga 18810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-map 8575  df-ga 18811

This theorem is referenced by:  gagrp  18813  gaset  18814  gagrpid  18815  gaf  18816  gaass  18818  ga0  18819  gaid  18820  subgga  18821  gass  18822  gasubg  18823  lactghmga  18928  sylow1lem2  19119  sylow2blem2  19141  sylow3lem1  19147