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

Definition df-dprd 18217
Description: Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 11-Jul-2019.)
Assertion
Ref Expression
df-dprd DProd = (𝑔 ∈ Grp, 𝑠 ∈ { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))} ↦ ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓)))
Distinct variable group:   𝑔,,𝑓,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-dprd
StepHypRef Expression
1 cdprd 18215 . 2 class DProd
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 17245 . . 3 class Grp
5 vh . . . . . . . 8 setvar
65cv 1474 . . . . . . 7 class
76cdm 5038 . . . . . 6 class dom
82cv 1474 . . . . . . 7 class 𝑔
9 csubg 17411 . . . . . . 7 class SubGrp
108, 9cfv 5804 . . . . . 6 class (SubGrp‘𝑔)
117, 10, 6wf 5800 . . . . 5 wff :dom ⟶(SubGrp‘𝑔)
12 vx . . . . . . . . . . 11 setvar 𝑥
1312cv 1474 . . . . . . . . . 10 class 𝑥
1413, 6cfv 5804 . . . . . . . . 9 class (𝑥)
15 vy . . . . . . . . . . . 12 setvar 𝑦
1615cv 1474 . . . . . . . . . . 11 class 𝑦
1716, 6cfv 5804 . . . . . . . . . 10 class (𝑦)
18 ccntz 17571 . . . . . . . . . . 11 class Cntz
198, 18cfv 5804 . . . . . . . . . 10 class (Cntz‘𝑔)
2017, 19cfv 5804 . . . . . . . . 9 class ((Cntz‘𝑔)‘(𝑦))
2114, 20wss 3540 . . . . . . . 8 wff (𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦))
2213csn 4125 . . . . . . . . 9 class {𝑥}
237, 22cdif 3537 . . . . . . . 8 class (dom ∖ {𝑥})
2421, 15, 23wral 2896 . . . . . . 7 wff 𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦))
256, 23cima 5041 . . . . . . . . . . 11 class ( “ (dom ∖ {𝑥}))
2625cuni 4372 . . . . . . . . . 10 class ( “ (dom ∖ {𝑥}))
27 cmrc 16066 . . . . . . . . . . 11 class mrCls
2810, 27cfv 5804 . . . . . . . . . 10 class (mrCls‘(SubGrp‘𝑔))
2926, 28cfv 5804 . . . . . . . . 9 class ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))
3014, 29cin 3539 . . . . . . . 8 class ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥}))))
31 c0g 15923 . . . . . . . . . 10 class 0g
328, 31cfv 5804 . . . . . . . . 9 class (0g𝑔)
3332csn 4125 . . . . . . . 8 class {(0g𝑔)}
3430, 33wceq 1475 . . . . . . 7 wff ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}
3524, 34wa 383 . . . . . 6 wff (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)})
3635, 12, 7wral 2896 . . . . 5 wff 𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)})
3711, 36wa 383 . . . 4 wff (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))
3837, 5cab 2596 . . 3 class { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))}
39 vf . . . . 5 setvar 𝑓
40 cfsupp 8158 . . . . . . 7 class finSupp
416, 32, 40wbr 4583 . . . . . 6 wff finSupp (0g𝑔)
423cv 1474 . . . . . . . 8 class 𝑠
4342cdm 5038 . . . . . . 7 class dom 𝑠
4413, 42cfv 5804 . . . . . . 7 class (𝑠𝑥)
4512, 43, 44cixp 7794 . . . . . 6 class X𝑥 ∈ dom 𝑠(𝑠𝑥)
4641, 5, 45crab 2900 . . . . 5 class {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)}
4739cv 1474 . . . . . 6 class 𝑓
48 cgsu 15924 . . . . . 6 class Σg
498, 47, 48co 6549 . . . . 5 class (𝑔 Σg 𝑓)
5039, 46, 49cmpt 4643 . . . 4 class (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓))
5150crn 5039 . . 3 class ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓))
522, 3, 4, 38, 51cmpt2 6551 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))} ↦ ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓)))
531, 52wceq 1475 1 wff DProd = (𝑔 ∈ Grp, 𝑠 ∈ { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))} ↦ ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmdprd  18219  dmdprd  18220  dprdval  18225
  Copyright terms: Public domain W3C validator