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

Theorem isga 19322
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 19337). 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 19321 . . 3 GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
21elmpocl 7674 . 2 ( ∈ (𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V))
3 fvexd 6922 . . . . . . 7 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) ∈ V)
4 simplr 769 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌)
5 id 22 . . . . . . . . . . 11 (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔))
6 simpl 482 . . . . . . . . . . . . 13 ((𝑔 = 𝐺𝑠 = 𝑌) → 𝑔 = 𝐺)
76fveq2d 6911 . . . . . . . . . . . 12 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺))
8 isga.1 . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
97, 8eqtr4di 2793 . . . . . . . . . . 11 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) = 𝑋)
105, 9sylan9eqr 2797 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋)
1110, 4xpeq12d 5720 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌))
124, 11oveq12d 7449 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠m (𝑏 × 𝑠)) = (𝑌m (𝑋 × 𝑌)))
13 simpll 767 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺)
1413fveq2d 6911 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = (0g𝐺))
15 isga.3 . . . . . . . . . . . . 13 0 = (0g𝐺)
1614, 15eqtr4di 2793 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g𝑔) = 0 )
1716oveq1d 7446 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g𝑔)𝑚𝑥) = ( 0 𝑚𝑥))
1817eqeq1d 2737 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥))
1913fveq2d 6911 . . . . . . . . . . . . . . . 16 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = (+g𝐺))
20 isga.2 . . . . . . . . . . . . . . . 16 + = (+g𝐺)
2119, 20eqtr4di 2793 . . . . . . . . . . . . . . 15 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g𝑔) = + )
2221oveqd 7448 . . . . . . . . . . . . . 14 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g𝑔)𝑧) = (𝑦 + 𝑧))
2322oveq1d 7446 . . . . . . . . . . . . 13 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥))
2423eqeq1d 2737 . . . . . . . . . . . 12 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2510, 24raleqbidv 3344 . . . . . . . . . . 11 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2610, 25raleqbidv 3344 . . . . . . . . . 10 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))
2718, 26anbi12d 632 . . . . . . . . 9 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
284, 27raleqbidv 3344 . . . . . . . 8 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))))
2912, 28rabeqbidv 3452 . . . . . . 7 (((𝑔 = 𝐺𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
303, 29csbied 3946 . . . . . 6 ((𝑔 = 𝐺𝑠 = 𝑌) → (Base‘𝑔) / 𝑏{𝑚 ∈ (𝑠m (𝑏 × 𝑠)) ∣ ∀𝑥𝑠 (((0g𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑏𝑧𝑏 ((𝑦(+g𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
31 ovex 7464 . . . . . . 7 (𝑌m (𝑋 × 𝑌)) ∈ V
3231rabex 5345 . . . . . 6 {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V
3330, 1, 32ovmpoa 7588 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
3433eleq2d 2825 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ∈ {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}))
35 oveq 7437 . . . . . . . 8 (𝑚 = → ( 0 𝑚𝑥) = ( 0 𝑥))
3635eqeq1d 2737 . . . . . . 7 (𝑚 = → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 𝑥) = 𝑥))
37 oveq 7437 . . . . . . . . 9 (𝑚 = → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) 𝑥))
38 oveq 7437 . . . . . . . . . 10 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧𝑚𝑥)))
39 oveq 7437 . . . . . . . . . . 11 (𝑚 = → (𝑧𝑚𝑥) = (𝑧 𝑥))
4039oveq2d 7447 . . . . . . . . . 10 (𝑚 = → (𝑦 (𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4138, 40eqtrd 2775 . . . . . . . . 9 (𝑚 = → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 (𝑧 𝑥)))
4237, 41eqeq12d 2751 . . . . . . . 8 (𝑚 = → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
43422ralbidv 3219 . . . . . . 7 (𝑚 = → (∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))
4436, 43anbi12d 632 . . . . . 6 (𝑚 = → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4544ralbidv 3176 . . . . 5 (𝑚 = → (∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4645elrab 3695 . . . 4 ( ∈ {𝑚 ∈ (𝑌m (𝑋 × 𝑌)) ∣ ∀𝑥𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))))
4734, 46bitrdi 287 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
48 simpr 484 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V)
498fvexi 6921 . . . . . 6 𝑋 ∈ V
50 xpexg 7769 . . . . . 6 ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5149, 48, 50sylancr 587 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V)
5248, 51elmapd 8879 . . . 4 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝑌m (𝑋 × 𝑌)) ↔ :(𝑋 × 𝑌)⟶𝑌))
5352anbi1d 631 . . 3 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ∈ (𝑌m (𝑋 × 𝑌)) ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥)))) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
5447, 53bitrd 279 . 2 ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ∈ (𝐺 GrpAct 𝑌) ↔ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
552, 54biadanii 822 1 ( ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥𝑌 (( 0 𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦 + 𝑧) 𝑥) = (𝑦 (𝑧 𝑥))))))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  {crab 3433  Vcvv 3478  csb 3908   × cxp 5687  wf 6559  cfv 6563  (class class class)co 7431  m cmap 8865  Basecbs 17245  +gcplusg 17298  0gc0g 17486  Grpcgrp 18964   GrpAct cga 19320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8867  df-ga 19321
This theorem is referenced by:  gagrp  19323  gaset  19324  gagrpid  19325  gaf  19326  gaass  19328  ga0  19329  gaid  19330  subgga  19331  gass  19332  gasubg  19333  lactghmga  19438  sylow1lem2  19632  sylow2blem2  19654  sylow3lem1  19660
  Copyright terms: Public domain W3C validator