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 19865
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 19863 . 2 class DProd
2 vg . . 3 setvar ๐‘”
3 vs . . 3 setvar ๐‘ 
4 cgrp 18819 . . 3 class Grp
5 vh . . . . . . . 8 setvar โ„Ž
65cv 1541 . . . . . . 7 class โ„Ž
76cdm 5677 . . . . . 6 class dom โ„Ž
82cv 1541 . . . . . . 7 class ๐‘”
9 csubg 19000 . . . . . . 7 class SubGrp
108, 9cfv 6544 . . . . . 6 class (SubGrpโ€˜๐‘”)
117, 10, 6wf 6540 . . . . 5 wff โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”)
12 vx . . . . . . . . . . 11 setvar ๐‘ฅ
1312cv 1541 . . . . . . . . . 10 class ๐‘ฅ
1413, 6cfv 6544 . . . . . . . . 9 class (โ„Žโ€˜๐‘ฅ)
15 vy . . . . . . . . . . . 12 setvar ๐‘ฆ
1615cv 1541 . . . . . . . . . . 11 class ๐‘ฆ
1716, 6cfv 6544 . . . . . . . . . 10 class (โ„Žโ€˜๐‘ฆ)
18 ccntz 19179 . . . . . . . . . . 11 class Cntz
198, 18cfv 6544 . . . . . . . . . 10 class (Cntzโ€˜๐‘”)
2017, 19cfv 6544 . . . . . . . . 9 class ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
2114, 20wss 3949 . . . . . . . 8 wff (โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
2213csn 4629 . . . . . . . . 9 class {๐‘ฅ}
237, 22cdif 3946 . . . . . . . 8 class (dom โ„Ž โˆ– {๐‘ฅ})
2421, 15, 23wral 3062 . . . . . . 7 wff โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ))
256, 23cima 5680 . . . . . . . . . . 11 class (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))
2625cuni 4909 . . . . . . . . . 10 class โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))
27 cmrc 17527 . . . . . . . . . . 11 class mrCls
2810, 27cfv 6544 . . . . . . . . . 10 class (mrClsโ€˜(SubGrpโ€˜๐‘”))
2926, 28cfv 6544 . . . . . . . . 9 class ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))
3014, 29cin 3948 . . . . . . . 8 class ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ}))))
31 c0g 17385 . . . . . . . . . 10 class 0g
328, 31cfv 6544 . . . . . . . . 9 class (0gโ€˜๐‘”)
3332csn 4629 . . . . . . . 8 class {(0gโ€˜๐‘”)}
3430, 33wceq 1542 . . . . . . 7 wff ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}
3524, 34wa 397 . . . . . 6 wff (โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)})
3635, 12, 7wral 3062 . . . . 5 wff โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)})
3711, 36wa 397 . . . 4 wff (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))
3837, 5cab 2710 . . 3 class {โ„Ž โˆฃ (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))}
39 vf . . . . 5 setvar ๐‘“
40 cfsupp 9361 . . . . . . 7 class finSupp
416, 32, 40wbr 5149 . . . . . 6 wff โ„Ž finSupp (0gโ€˜๐‘”)
423cv 1541 . . . . . . . 8 class ๐‘ 
4342cdm 5677 . . . . . . 7 class dom ๐‘ 
4413, 42cfv 6544 . . . . . . 7 class (๐‘ โ€˜๐‘ฅ)
4512, 43, 44cixp 8891 . . . . . 6 class X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ)
4641, 5, 45crab 3433 . . . . 5 class {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)}
4739cv 1541 . . . . . 6 class ๐‘“
48 cgsu 17386 . . . . . 6 class ฮฃg
498, 47, 48co 7409 . . . . 5 class (๐‘” ฮฃg ๐‘“)
5039, 46, 49cmpt 5232 . . . 4 class (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“))
5150crn 5678 . . 3 class ran (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“))
522, 3, 4, 38, 51cmpo 7411 . 2 class (๐‘” โˆˆ Grp, ๐‘  โˆˆ {โ„Ž โˆฃ (โ„Ž:dom โ„ŽโŸถ(SubGrpโ€˜๐‘”) โˆง โˆ€๐‘ฅ โˆˆ dom โ„Ž(โˆ€๐‘ฆ โˆˆ (dom โ„Ž โˆ– {๐‘ฅ})(โ„Žโ€˜๐‘ฅ) โŠ† ((Cntzโ€˜๐‘”)โ€˜(โ„Žโ€˜๐‘ฆ)) โˆง ((โ„Žโ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐‘”))โ€˜โˆช (โ„Ž โ€œ (dom โ„Ž โˆ– {๐‘ฅ})))) = {(0gโ€˜๐‘”)}))} โ†ฆ ran (๐‘“ โˆˆ {โ„Ž โˆˆ X๐‘ฅ โˆˆ dom ๐‘ (๐‘ โ€˜๐‘ฅ) โˆฃ โ„Ž finSupp (0gโ€˜๐‘”)} โ†ฆ (๐‘” ฮฃg ๐‘“)))
531, 52wceq 1542 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  19867  dmdprd  19868  dprdval  19873
  Copyright terms: Public domain W3C validator