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

Theorem isga 19149
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 19164). 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 19148 . . 3 GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
21elmpocl 7644 . 2 ( ∈ (𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V))
3 fvexd 6903 . . . . . . 7 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) ∈ V)
4 simplr 767 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌)
5 id 22 . . . . . . . . . . 11 (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔))
6 simpl 483 . . . . . . . . . . . . 13 ((𝑔 = 𝐺𝑠 = 𝑌) → 𝑔 = 𝐺)
76fveq2d 6892 . . . . . . . . . . . 12 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺))
8 isga.1 . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
97, 8eqtr4di 2790 . . . . . . . . . . 11 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = 𝑋)
105, 9sylan9eqr 2794 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋)
1110, 4xpeq12d 5706 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌))
124, 11oveq12d 7423 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠m (𝑏 × 𝑠)) = (𝑌m (𝑋 × 𝑌)))
13 simpll 765 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺)
1413fveq2d 6892 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = (0g𝐺))
15 isga.3 . . . . . . . . . . . . 13 0 = (0g𝐺)
1614, 15eqtr4di 2790 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = 0 )
1716oveq1d 7420 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g𝑔)𝑚𝑥) = ( 0 𝑚𝑥))
1817eqeq1d 2734 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥))
1913fveq2d 6892 . . . . . . . . . . . . . . . 16 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = (+g𝐺))
20 isga.2 . . . . . . . . . . . . . . . 16 + = (+g𝐺)
2119, 20eqtr4di 2790 . . . . . . . . . . . . . . 15 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = + )
2221oveqd 7422 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g𝑔)𝑧) = (𝑦 + 𝑧))
2322oveq1d 7420 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥))
2423eqeq1d 2734 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2510, 24raleqbidv 3342 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2610, 25raleqbidv 3342 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2718, 26anbi12d 631 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
284, 27raleqbidv 3342 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
2912, 28rabeqbidv 3449 . . . . . . 7 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
303, 29csbied 3930 . . . . . 6 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
31 ovex 7438 . . . . . . 7 (𝑌m (𝑋 × 𝑌)) ∈ V
3231rabex 5331 . . . . . 6 {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V
3330, 1, 32ovmpoa 7559 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
3433eleq2d 2819 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ∈ {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}))
35 oveq 7411 . . . . . . . 8 (𝑚 = → ( 0 𝑚𝑥) = ( 0 𝑥))
3635eqeq1d 2734 . . . . . . 7 (𝑚 = → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 𝑥) = 𝑥))
37 oveq 7411 . . . . . . . . 9 (𝑚 = → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) 𝑥))
38 oveq 7411 . . . . . . . . . 10 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧𝑚𝑥)))
39 oveq 7411 . . . . . . . . . . 11 (𝑚 = → (𝑧𝑚𝑥) = (𝑧 𝑥))
4039oveq2d 7421 . . . . . . . . . 10 (𝑚 = → (𝑦 (𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4138, 40eqtrd 2772 . . . . . . . . 9 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4237, 41eqeq12d 2748 . . . . . . . 8 (𝑚 = → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
43422ralbidv 3218 . . . . . . 7 (𝑚 = → (∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
4436, 43anbi12d 631 . . . . . 6 (𝑚 = → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4544ralbidv 3177 . . . . 5 (𝑚 = → (∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4645elrab 3682 . . . 4 ( ∈ {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4734, 46bitrdi 286 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
48 simpr 485 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V)
498fvexi 6902 . . . . . 6 𝑋 ∈ V
50 xpexg 7733 . . . . . 6 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5149, 48, 50sylancr 587 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5248, 51elmapd 8830 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝑌m (𝑋 × 𝑌)) ↔ :(𝑋 × 𝑌)⟶𝑌))
5352anbi1d 630 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
5447, 53bitrd 278 . 2 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
552, 54biadanii 820 1 ( ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  {crab 3432  Vcvv 3474  csb 3892   × cxp 5673  wf 6536  cfv 6540  (class class class)co 7405  m cmap 8816  Basecbs 17140  +gcplusg 17193  0gc0g 17381  Grpcgrp 18815   GrpAct cga 19147
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8818  df-ga 19148
This theorem is referenced by:  gagrp  19150  gaset  19151  gagrpid  19152  gaf  19153  gaass  19155  ga0  19156  gaid  19157  subgga  19158  gass  19159  gasubg  19160  lactghmga  19267  sylow1lem2  19461  sylow2blem2  19483  sylow3lem1  19489
  Copyright terms: Public domain W3C validator