MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isga Structured version   Visualization version   GIF version

Theorem isga 17989
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 18004). 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.
StepHypRef Expression
1 df-ga 17988 . . 3 GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
21elmpt2cl 7074 . 2 ( ∈ (𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V))
3 fvexd 6390 . . . . . . 7 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) ∈ V)
4 simplr 785 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌)
5 id 22 . . . . . . . . . . 11 (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔))
6 simpl 474 . . . . . . . . . . . . 13 ((𝑔 = 𝐺𝑠 = 𝑌) → 𝑔 = 𝐺)
76fveq2d 6379 . . . . . . . . . . . 12 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺))
8 isga.1 . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
97, 8syl6eqr 2817 . . . . . . . . . . 11 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = 𝑋)
105, 9sylan9eqr 2821 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋)
1110, 4xpeq12d 5308 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌))
124, 11oveq12d 6860 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠𝑚 (𝑏 × 𝑠)) = (𝑌𝑚 (𝑋 × 𝑌)))
13 simpll 783 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺)
1413fveq2d 6379 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = (0g𝐺))
15 isga.3 . . . . . . . . . . . . 13 0 = (0g𝐺)
1614, 15syl6eqr 2817 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = 0 )
1716oveq1d 6857 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g𝑔)𝑚𝑥) = ( 0 𝑚𝑥))
1817eqeq1d 2767 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥))
1913fveq2d 6379 . . . . . . . . . . . . . . . 16 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = (+g𝐺))
20 isga.2 . . . . . . . . . . . . . . . 16 + = (+g𝐺)
2119, 20syl6eqr 2817 . . . . . . . . . . . . . . 15 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = + )
2221oveqd 6859 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g𝑔)𝑧) = (𝑦 + 𝑧))
2322oveq1d 6857 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥))
2423eqeq1d 2767 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2510, 24raleqbidv 3300 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2610, 25raleqbidv 3300 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2718, 26anbi12d 624 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
284, 27raleqbidv 3300 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
2912, 28rabeqbidv 3344 . . . . . . 7 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
303, 29csbied 3718 . . . . . 6 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
31 ovex 6874 . . . . . . 7 (𝑌𝑚 (𝑋 × 𝑌)) ∈ V
3231rabex 4973 . . . . . 6 {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V
3330, 1, 32ovmpt2a 6989 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
3433eleq2d 2830 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ∈ {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}))
35 oveq 6848 . . . . . . . 8 (𝑚 = → ( 0 𝑚𝑥) = ( 0 𝑥))
3635eqeq1d 2767 . . . . . . 7 (𝑚 = → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 𝑥) = 𝑥))
37 oveq 6848 . . . . . . . . 9 (𝑚 = → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) 𝑥))
38 oveq 6848 . . . . . . . . . 10 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧𝑚𝑥)))
39 oveq 6848 . . . . . . . . . . 11 (𝑚 = → (𝑧𝑚𝑥) = (𝑧 𝑥))
4039oveq2d 6858 . . . . . . . . . 10 (𝑚 = → (𝑦 (𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4138, 40eqtrd 2799 . . . . . . . . 9 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4237, 41eqeq12d 2780 . . . . . . . 8 (𝑚 = → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
43422ralbidv 3136 . . . . . . 7 (𝑚 = → (∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
4436, 43anbi12d 624 . . . . . 6 (𝑚 = → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4544ralbidv 3133 . . . . 5 (𝑚 = → (∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4645elrab 3519 . . . 4 ( ∈ {𝑚 ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4734, 46syl6bb 278 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
48 simpr 477 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V)
498fvexi 6389 . . . . . 6 𝑋 ∈ V
50 xpexg 7158 . . . . . 6 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5149, 48, 50sylancr 581 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5248, 51elmapd 8074 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝑌𝑚 (𝑋 × 𝑌)) ↔ :(𝑋 × 𝑌)⟶𝑌))
5352anbi1d 623 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ∈ (𝑌𝑚 (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
5447, 53bitrd 270 . 2 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
552, 54biadan2 853 1 ( ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  {crab 3059  Vcvv 3350  csb 3691   × cxp 5275  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  Basecbs 16132  +gcplusg 16216  0gc0g 16368  Grpcgrp 17691   GrpAct cga 17987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-map 8062  df-ga 17988
This theorem is referenced by:  gagrp  17990  gaset  17991  gagrpid  17992  gaf  17993  gaass  17995  ga0  17996  gaid  17997  subgga  17998  gass  17999  gasubg  18000  lactghmga  18089  sylow1lem2  18280  sylow2blem2  18302  sylow3lem1  18308
  Copyright terms: Public domain W3C validator