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

Theorem gaid 18408
Description: The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
Hypothesis
Ref Expression
gaid.1 𝑋 = (Base‘𝐺)
Assertion
Ref Expression
gaid ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆))

Proof of Theorem gaid
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3491 . . 3 (𝑆𝑉𝑆 ∈ V)
21anim2i 618 . 2 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
3 gaid.1 . . . . . . . 8 𝑋 = (Base‘𝐺)
4 eqid 2820 . . . . . . . 8 (0g𝐺) = (0g𝐺)
53, 4grpidcl 18110 . . . . . . 7 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
65adantr 483 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (0g𝐺) ∈ 𝑋)
7 ovres 7292 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = ((0g𝐺)2nd 𝑥))
8 df-ov 7136 . . . . . . . 8 ((0g𝐺)2nd 𝑥) = (2nd ‘⟨(0g𝐺), 𝑥⟩)
9 fvex 6659 . . . . . . . . 9 (0g𝐺) ∈ V
10 vex 3476 . . . . . . . . 9 𝑥 ∈ V
119, 10op2nd 7676 . . . . . . . 8 (2nd ‘⟨(0g𝐺), 𝑥⟩) = 𝑥
128, 11eqtri 2843 . . . . . . 7 ((0g𝐺)2nd 𝑥) = 𝑥
137, 12syl6eq 2871 . . . . . 6 (((0g𝐺) ∈ 𝑋𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
146, 13sylan 582 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
15 simprl 769 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
16 simplr 767 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑥𝑆)
17 ovres 7292 . . . . . . . . 9 ((𝑦𝑋𝑥𝑆) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦2nd 𝑥))
18 df-ov 7136 . . . . . . . . . 10 (𝑦2nd 𝑥) = (2nd ‘⟨𝑦, 𝑥⟩)
19 vex 3476 . . . . . . . . . . 11 𝑦 ∈ V
2019, 10op2nd 7676 . . . . . . . . . 10 (2nd ‘⟨𝑦, 𝑥⟩) = 𝑥
2118, 20eqtri 2843 . . . . . . . . 9 (𝑦2nd 𝑥) = 𝑥
2217, 21syl6eq 2871 . . . . . . . 8 ((𝑦𝑋𝑥𝑆) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
2315, 16, 22syl2anc 586 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
24 simprr 771 . . . . . . . . 9 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
25 ovres 7292 . . . . . . . . . 10 ((𝑧𝑋𝑥𝑆) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑧2nd 𝑥))
26 df-ov 7136 . . . . . . . . . . 11 (𝑧2nd 𝑥) = (2nd ‘⟨𝑧, 𝑥⟩)
27 vex 3476 . . . . . . . . . . . 12 𝑧 ∈ V
2827, 10op2nd 7676 . . . . . . . . . . 11 (2nd ‘⟨𝑧, 𝑥⟩) = 𝑥
2926, 28eqtri 2843 . . . . . . . . . 10 (𝑧2nd 𝑥) = 𝑥
3025, 29syl6eq 2871 . . . . . . . . 9 ((𝑧𝑋𝑥𝑆) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
3124, 16, 30syl2anc 586 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
3231oveq2d 7149 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)) = (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥))
33 eqid 2820 . . . . . . . . . . 11 (+g𝐺) = (+g𝐺)
343, 33grpcl 18090 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
35343expb 1116 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
3635ad4ant14 750 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
37 ovres 7292 . . . . . . . . 9 (((𝑦(+g𝐺)𝑧) ∈ 𝑋𝑥𝑆) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = ((𝑦(+g𝐺)𝑧)2nd 𝑥))
38 df-ov 7136 . . . . . . . . . 10 ((𝑦(+g𝐺)𝑧)2nd 𝑥) = (2nd ‘⟨(𝑦(+g𝐺)𝑧), 𝑥⟩)
39 ovex 7166 . . . . . . . . . . 11 (𝑦(+g𝐺)𝑧) ∈ V
4039, 10op2nd 7676 . . . . . . . . . 10 (2nd ‘⟨(𝑦(+g𝐺)𝑧), 𝑥⟩) = 𝑥
4138, 40eqtri 2843 . . . . . . . . 9 ((𝑦(+g𝐺)𝑧)2nd 𝑥) = 𝑥
4237, 41syl6eq 2871 . . . . . . . 8 (((𝑦(+g𝐺)𝑧) ∈ 𝑋𝑥𝑆) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
4336, 16, 42syl2anc 586 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
4423, 32, 433eqtr4rd 2866 . . . . . 6 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))
4544ralrimivva 3178 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))
4614, 45jca 514 . . . 4 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))
4746ralrimiva 3169 . . 3 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))
48 f2ndres 7692 . . 3 (2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆
4947, 48jctil 522 . 2 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → ((2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))))
503, 33, 4isga 18400 . 2 ((2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ((2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))))
512, 49, 50sylanbrc 585 1 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1537  wcel 2114  wral 3125  Vcvv 3473  cop 4549   × cxp 5529  cres 5533  wf 6327  cfv 6331  (class class class)co 7133  2nd c2nd 7666  Basecbs 16462  +gcplusg 16544  0gc0g 16692  Grpcgrp 18082   GrpAct cga 18398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-2nd 7668  df-map 8386  df-0g 16694  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-grp 18085  df-ga 18399
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator