Metamath Proof Explorer

Definition df-dprd

Description: Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Assertion df-dprd DProd = ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdprd ⊢ DProd
1 vg ⊢ 𝑔
2 cgrp ⊢ Grp
3 vs ⊢ 𝑠
4 vh ⊢ ℎ
5 4 cv ⊢ ℎ
6 5 cdm ⊢ dom ℎ
7 csubg ⊢ SubGrp
8 1 cv ⊢ 𝑔
9 8 7 cfv ⊢ ( SubGrp ‘ 𝑔 )
10 6 9 5 wf ⊢ ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 )
11 vx ⊢ 𝑥
12 vy ⊢ 𝑦
13 11 cv ⊢ 𝑥
14 13 csn ⊢ { 𝑥 }
15 6 14 cdif ⊢ ( dom ℎ ∖ { 𝑥 } )
16 13 5 cfv ⊢ ( ℎ ‘ 𝑥 )
17 ccntz ⊢ Cntz
18 8 17 cfv ⊢ ( Cntz ‘ 𝑔 )
19 12 cv ⊢ 𝑦
20 19 5 cfv ⊢ ( ℎ ‘ 𝑦 )
21 20 18 cfv ⊢ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) )
22 16 21 wss ⊢ ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) )
23 22 12 15 wral ⊢ ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) )
24 cmrc ⊢ mrCls
25 9 24 cfv ⊢ ( mrCls ‘ ( SubGrp ‘ 𝑔 ) )
26 5 15 cima ⊢ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) )
27 26 cuni ⊢ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) )
28 27 25 cfv ⊢ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) )
29 16 28 cin ⊢ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) )
30 c0g ⊢ 0g
31 8 30 cfv ⊢ ( 0g ‘ 𝑔 )
32 31 csn ⊢ { ( 0g ‘ 𝑔 ) }
33 29 32 wceq ⊢ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) }
34 23 33 wa ⊢ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } )
35 34 11 6 wral ⊢ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } )
36 10 35 wa ⊢ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) )
37 36 4 cab ⊢ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) }
38 vf ⊢ 𝑓
39 3 cv ⊢ 𝑠
40 39 cdm ⊢ dom 𝑠
41 13 39 cfv ⊢ ( 𝑠 ‘ 𝑥 )
42 11 40 41 cixp ⊢ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 )
43 cfsupp ⊢ finSupp
44 5 31 43 wbr ⊢ ℎ finSupp ( 0g ‘ 𝑔 )
45 44 4 42 crab ⊢ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) }
46 cgsu ⊢ Σg
47 38 cv ⊢ 𝑓
48 8 47 46 co ⊢ ( 𝑔 Σg 𝑓 )
49 38 45 48 cmpt ⊢ ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) )
50 49 crn ⊢ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) )
51 1 3 2 37 50 cmpo ⊢ ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
52 0 51 wceq ⊢ DProd = ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )