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 19864
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 19862 . 2 class DProd
2 vg . . 3 setvar ๐‘”
3 vs . . 3 setvar ๐‘ 
4 cgrp 18818 . . 3 class Grp
5 vh . . . . . . . 8 setvar โ„Ž
65cv 1540 . . . . . . 7 class โ„Ž
76cdm 5676 . . . . . 6 class dom โ„Ž
82cv 1540 . . . . . . 7 class ๐‘”
9 csubg 18999 . . . . . . 7 class SubGrp
108, 9cfv 6543 . . . . . 6 class (SubGrpโ€˜๐‘”)
117, 10, 6wf 6539 . . . . 5 wff โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”)
12 vx . . . . . . . . . . 11 setvar ๐‘ฅ
1312cv 1540 . . . . . . . . . 10 class ๐‘ฅ
1413, 6cfv 6543 . . . . . . . . 9 class (โ„Žโ€˜๐‘ฅ)
15 vy . . . . . . . . . . . 12 setvar ๐‘ฆ
1615cv 1540 . . . . . . . . . . 11 class ๐‘ฆ
1716, 6cfv 6543 . . . . . . . . . 10 class (โ„Žโ€˜๐‘ฆ)
18 ccntz 19178 . . . . . . . . . . 11 class Cntz
198, 18cfv 6543 . . . . . . . . . 10 class (Cntzโ€˜๐‘”)
2017, 19cfv 6543 . . . . . . . . 9 class ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
2114, 20wss 3948 . . . . . . . 8 wff (โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
2213csn 4628 . . . . . . . . 9 class {๐‘ฅ}
237, 22cdif 3945 . . . . . . . 8 class (dom โ„Ž โˆ– {๐‘ฅ})
2421, 15, 23wral 3061 . . . . . . 7 wff โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
256, 23cima 5679 . . . . . . . . . . 11 class (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))
2625cuni 4908 . . . . . . . . . 10 class โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))
27 cmrc 17526 . . . . . . . . . . 11 class mrCls
2810, 27cfv 6543 . . . . . . . . . 10 class (mrClsโ€˜(SubGrpโ€˜๐‘”))
2926, 28cfv 6543 . . . . . . . . 9 class ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))
3014, 29cin 3947 . . . . . . . 8 class ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))))
31 c0g 17384 . . . . . . . . . 10 class 0g
328, 31cfv 6543 . . . . . . . . 9 class (0gโ€˜๐‘”)
3332csn 4628 . . . . . . . 8 class {(0gโ€˜๐‘”)}
3430, 33wceq 1541 . . . . . . 7 wff ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}
3524, 34wa 396 . . . . . 6 wff (โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)})
3635, 12, 7wral 3061 . . . . 5 wff โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)})
3711, 36wa 396 . . . 4 wff (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))
3837, 5cab 2709 . . 3 class {โ„Ž โˆฃ (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))}
39 vf . . . . 5 setvar ๐‘“
40 cfsupp 9360 . . . . . . 7 class finSupp
416, 32, 40wbr 5148 . . . . . 6 wff โ„Ž finSupp (0gโ€˜๐‘”)
423cv 1540 . . . . . . . 8 class ๐‘ 
4342cdm 5676 . . . . . . 7 class dom ๐‘ 
4413, 42cfv 6543 . . . . . . 7 class (๐‘ โ€˜๐‘ฅ)
4512, 43, 44cixp 8890 . . . . . 6 class X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ)
4641, 5, 45crab 3432 . . . . 5 class {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)}
4739cv 1540 . . . . . 6 class ๐‘“
48 cgsu 17385 . . . . . 6 class ฮฃg
498, 47, 48co 7408 . . . . 5 class (๐‘” ฮฃg ๐‘“)
5039, 46, 49cmpt 5231 . . . 4 class (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“))
5150crn 5677 . . 3 class ran (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“))
522, 3, 4, 38, 51cmpo 7410 . 2 class (๐‘” โˆˆ Grp, ๐‘  โˆˆ {โ„Ž โˆฃ (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))} โ†ฆ ran (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“)))
531, 52wceq 1541 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  19866  dmdprd  19867  dprdval  19872
  Copyright terms: Public domain W3C validator