Theorem isga 19232

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 19247). 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 19231	. . 3 ⊢ GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
2	1	elmpocl 7609	. 2 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V))
3		fvexd 6857	. . . . . . 7 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) ∈ V)
4		simplr 769	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌)
5		id 22	. . . . . . . . . . 11 ⊢ (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔))
6		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → 𝑔 = 𝐺)
7	6	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺))
8		isga.1	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝐺)
9	7, 8	eqtr4di 2790	. . . . . . . . . . 11 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = 𝑋)
10	5, 9	sylan9eqr 2794	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋)
11	10, 4	xpeq12d 5663	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌))
12	4, 11	oveq12d 7386	. . . . . . . 8 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠 ↑m (𝑏 × 𝑠)) = (𝑌 ↑m (𝑋 × 𝑌)))
13		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺)
14	13	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = (0g‘𝐺))
15		isga.3	. . . . . . . . . . . . 13 ⊢ 0 = (0g‘𝐺)
16	14, 15	eqtr4di 2790	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = 0 )
17	16	oveq1d 7383	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g‘𝑔)𝑚𝑥) = ( 0 𝑚𝑥))
18	17	eqeq1d 2739	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g‘𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥))
19	13	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = (+g‘𝐺))
20		isga.2	. . . . . . . . . . . . . . . 16 ⊢ + = (+g‘𝐺)
21	19, 20	eqtr4di 2790	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = + )
22	21	oveqd 7385	. . . . . . . . . . . . . 14 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g‘𝑔)𝑧) = (𝑦 + 𝑧))
23	22	oveq1d 7383	. . . . . . . . . . . . 13 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥))
24	23	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
25	10, 24	raleqbidv 3318	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
26	10, 25	raleqbidv 3318	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
27	18, 26	anbi12d 633	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
28	4, 27	raleqbidv 3318	. . . . . . . 8 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
29	12, 28	rabeqbidv 3419	. . . . . . 7 ⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
30	3, 29	csbied 3887	. . . . . 6 ⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
31		ovex 7401	. . . . . . 7 ⊢ (𝑌 ↑m (𝑋 × 𝑌)) ∈ V
32	31	rabex 5286	. . . . . 6 ⊢ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V
33	30, 1, 32	ovmpoa 7523	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
34	33	eleq2d 2823	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ⊕ ∈ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}))
35		oveq 7374	. . . . . . . 8 ⊢ (𝑚 = ⊕ → ( 0 𝑚𝑥) = ( 0 ⊕ 𝑥))
36	35	eqeq1d 2739	. . . . . . 7 ⊢ (𝑚 = ⊕ → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 ⊕ 𝑥) = 𝑥))
37		oveq 7374	. . . . . . . . 9 ⊢ (𝑚 = ⊕ → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) ⊕ 𝑥))
38		oveq 7374	. . . . . . . . . 10 ⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧𝑚𝑥)))
39		oveq 7374	. . . . . . . . . . 11 ⊢ (𝑚 = ⊕ → (𝑧𝑚𝑥) = (𝑧 ⊕ 𝑥))
40	39	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑚 = ⊕ → (𝑦 ⊕ (𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))
41	38, 40	eqtrd 2772	. . . . . . . . 9 ⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))
42	37, 41	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑚 = ⊕ → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))
43	42	2ralbidv 3202	. . . . . . 7 ⊢ (𝑚 = ⊕ → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))
44	36, 43	anbi12d 633	. . . . . 6 ⊢ (𝑚 = ⊕ → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
45	44	ralbidv 3161	. . . . 5 ⊢ (𝑚 = ⊕ → (∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
46	45	elrab 3648	. . . 4 ⊢ ( ⊕ ∈ {𝑚 ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))
47	34, 46	bitrdi 287	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
48		simpr 484	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V)
49	8	fvexi 6856	. . . . . 6 ⊢ 𝑋 ∈ V
50		xpexg 7705	. . . . . 6 ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
51	49, 48, 50	sylancr 588	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
52	48, 51	elmapd 8789	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌))
53	52	anbi1d 632	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ⊕ ∈ (𝑌 ↑m (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
54	47, 53	bitrd 279	. 2 ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
55	2, 54	biadanii 822	1 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3401  Vcvv 3442  ⦋csb 3851   × cxp 5630  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   ↑_m cmap 8775  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Grpcgrp 18875   GrpAct cga 19230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777  df-ga 19231

This theorem is referenced by:  gagrp  19233  gaset  19234  gagrpid  19235  gaf  19236  gaass  19238  ga0  19239  gaid  19240  subgga  19241  gass  19242  gasubg  19243  lactghmga  19346  sylow1lem2  19540  sylow2blem2  19562  sylow3lem1  19568  conjga  33263  mplvrpmga  33721