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

Theorem gaid 18548
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 3416 . . 3 (𝑆𝑉𝑆 ∈ V)
21anim2i 620 . 2 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (𝐺 ∈ Grp ∧ 𝑆 ∈ V))
3 gaid.1 . . . . . . . 8 𝑋 = (Base‘𝐺)
4 eqid 2738 . . . . . . . 8 (0g𝐺) = (0g𝐺)
53, 4grpidcl 18250 . . . . . . 7 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
65adantr 484 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (0g𝐺) ∈ 𝑋)
7 ovres 7331 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = ((0g𝐺)2nd 𝑥))
8 df-ov 7174 . . . . . . . 8 ((0g𝐺)2nd 𝑥) = (2nd ‘⟨(0g𝐺), 𝑥⟩)
9 fvex 6688 . . . . . . . . 9 (0g𝐺) ∈ V
10 vex 3402 . . . . . . . . 9 𝑥 ∈ V
119, 10op2nd 7724 . . . . . . . 8 (2nd ‘⟨(0g𝐺), 𝑥⟩) = 𝑥
128, 11eqtri 2761 . . . . . . 7 ((0g𝐺)2nd 𝑥) = 𝑥
137, 12eqtrdi 2789 . . . . . 6 (((0g𝐺) ∈ 𝑋𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
146, 13sylan 583 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → ((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
15 simprl 771 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
16 simplr 769 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑥𝑆)
17 ovres 7331 . . . . . . . . 9 ((𝑦𝑋𝑥𝑆) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦2nd 𝑥))
18 df-ov 7174 . . . . . . . . . 10 (𝑦2nd 𝑥) = (2nd ‘⟨𝑦, 𝑥⟩)
19 vex 3402 . . . . . . . . . . 11 𝑦 ∈ V
2019, 10op2nd 7724 . . . . . . . . . 10 (2nd ‘⟨𝑦, 𝑥⟩) = 𝑥
2118, 20eqtri 2761 . . . . . . . . 9 (𝑦2nd 𝑥) = 𝑥
2217, 21eqtrdi 2789 . . . . . . . 8 ((𝑦𝑋𝑥𝑆) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
2315, 16, 22syl2anc 587 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
24 simprr 773 . . . . . . . . 9 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
25 ovres 7331 . . . . . . . . . 10 ((𝑧𝑋𝑥𝑆) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑧2nd 𝑥))
26 df-ov 7174 . . . . . . . . . . 11 (𝑧2nd 𝑥) = (2nd ‘⟨𝑧, 𝑥⟩)
27 vex 3402 . . . . . . . . . . . 12 𝑧 ∈ V
2827, 10op2nd 7724 . . . . . . . . . . 11 (2nd ‘⟨𝑧, 𝑥⟩) = 𝑥
2926, 28eqtri 2761 . . . . . . . . . 10 (𝑧2nd 𝑥) = 𝑥
3025, 29eqtrdi 2789 . . . . . . . . 9 ((𝑧𝑋𝑥𝑆) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
3124, 16, 30syl2anc 587 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑧(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
3231oveq2d 7187 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)) = (𝑦(2nd ↾ (𝑋 × 𝑆))𝑥))
33 eqid 2738 . . . . . . . . . . 11 (+g𝐺) = (+g𝐺)
343, 33grpcl 18228 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
35343expb 1121 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
3635ad4ant14 752 . . . . . . . 8 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(+g𝐺)𝑧) ∈ 𝑋)
37 ovres 7331 . . . . . . . . 9 (((𝑦(+g𝐺)𝑧) ∈ 𝑋𝑥𝑆) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = ((𝑦(+g𝐺)𝑧)2nd 𝑥))
38 df-ov 7174 . . . . . . . . . 10 ((𝑦(+g𝐺)𝑧)2nd 𝑥) = (2nd ‘⟨(𝑦(+g𝐺)𝑧), 𝑥⟩)
39 ovex 7204 . . . . . . . . . . 11 (𝑦(+g𝐺)𝑧) ∈ V
4039, 10op2nd 7724 . . . . . . . . . 10 (2nd ‘⟨(𝑦(+g𝐺)𝑧), 𝑥⟩) = 𝑥
4138, 40eqtri 2761 . . . . . . . . 9 ((𝑦(+g𝐺)𝑧)2nd 𝑥) = 𝑥
4237, 41eqtrdi 2789 . . . . . . . 8 (((𝑦(+g𝐺)𝑧) ∈ 𝑋𝑥𝑆) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
4336, 16, 42syl2anc 587 . . . . . . 7 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥)
4423, 32, 433eqtr4rd 2784 . . . . . 6 ((((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))
4544ralrimivva 3103 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))
4614, 45jca 515 . . . 4 (((𝐺 ∈ Grp ∧ 𝑆𝑉) ∧ 𝑥𝑆) → (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))
4746ralrimiva 3096 . . 3 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))
48 f2ndres 7740 . . 3 (2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆
4947, 48jctil 523 . 2 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → ((2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥)))))
503, 33, 4isga 18540 . 2 ((2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆) ↔ ((𝐺 ∈ Grp ∧ 𝑆 ∈ V) ∧ ((2nd ↾ (𝑋 × 𝑆)):(𝑋 × 𝑆)⟶𝑆 ∧ ∀𝑥𝑆 (((0g𝐺)(2nd ↾ (𝑋 × 𝑆))𝑥) = 𝑥 ∧ ∀𝑦𝑋𝑧𝑋 ((𝑦(+g𝐺)𝑧)(2nd ↾ (𝑋 × 𝑆))𝑥) = (𝑦(2nd ↾ (𝑋 × 𝑆))(𝑧(2nd ↾ (𝑋 × 𝑆))𝑥))))))
512, 49, 50sylanbrc 586 1 ((𝐺 ∈ Grp ∧ 𝑆𝑉) → (2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2113  wral 3053  Vcvv 3398  cop 4523   × cxp 5524  cres 5528  wf 6336  cfv 6340  (class class class)co 7171  2nd c2nd 7714  Basecbs 16587  +gcplusg 16669  0gc0g 16817  Grpcgrp 18220   GrpAct cga 18538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-fv 6348  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-2nd 7716  df-map 8440  df-0g 16819  df-mgm 17969  df-sgrp 18018  df-mnd 18029  df-grp 18223  df-ga 18539
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator