Metamath Proof Explorer

Theorem dmdprd

Description: The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016) (Proof shortened by AV, 11-Jul-2019)

Ref Expression
Hypotheses dmdprd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
dmdprd.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dmdprd.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion dmdprd ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )

Proof

Step Hyp Ref Expression
1 dmdprd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 dmdprd.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 dmdprd.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4 elex ⊢ ( 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } → 𝑆 ∈ V )
5 4 a1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } → 𝑆 ∈ V ) )
6 fex ⊢ ( ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ 𝐼 ∈ 𝑉 ) → 𝑆 ∈ V )
7 6 expcom ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ V ) )
8 7 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ V ) )
9 8 adantrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) → 𝑆 ∈ V ) )
10 df-sbc ⊢ ( [ 𝑆 / ℎ ] ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ↔ 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } )
11 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑆 ∈ V ) → 𝑆 ∈ V )
12 simpr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ℎ = 𝑆 )
13 12 dmeqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → dom ℎ = dom 𝑆 )
14 simplr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → dom 𝑆 = 𝐼 )
15 13 14 eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → dom ℎ = 𝐼 )
16 12 15 feq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ↔ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ) )
17 15 difeq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( dom ℎ ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑥 } ) )
18 12 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ℎ ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
19 12 fveq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ℎ ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
20 19 fveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
21 18 20 sseq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
22 17 21 raleqbidv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
23 12 17 imaeq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) = ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
24 23 unieqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) = ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) )
25 24 fveq2d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
26 18 25 ineq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
27 26 eqeq1d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ↔ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) )
28 22 27 anbi12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ↔ ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) )
29 15 28 raleqbidv ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) )
30 16 29 anbi12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ ℎ = 𝑆 ) → ( ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
31 30 adantlr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑆 ∈ V ) ∧ ℎ = 𝑆 ) → ( ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
32 11 31 sbcied ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑆 ∈ V ) → ( [ 𝑆 / ℎ ] ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
33 10 32 bitr3id ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) ∧ 𝑆 ∈ V ) → ( 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
34 33 ex ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝑆 ∈ V → ( 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) ) )
35 5 9 34 pm5.21ndd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ↔ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
36 35 anbi2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) ) )
37 df-br ⊢ ( 𝐺 dom DProd 𝑆 ↔ ⟨ 𝐺 , 𝑆 ⟩ ∈ dom DProd )
38 fvex ⊢ ( 𝑠 ‘ 𝑥 ) ∈ V
39 38 rgenw ⊢ ∀ 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∈ V
40 ixpexg ⊢ ( ∀ 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∈ V → X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∈ V )
41 39 40 ax-mp ⊢ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∈ V
42 41 mptrabex ⊢ ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
43 42 rnex ⊢ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
44 43 rgen2w ⊢ ∀ 𝑔 ∈ Grp ∀ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V
45 df-dprd ⊢ DProd = ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
46 45 fmpox ⊢ ( ∀ 𝑔 ∈ Grp ∀ 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ∈ V ↔ DProd : ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) ⟶ V )
47 44 46 mpbi ⊢ DProd : ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) ⟶ V
48 47 fdmi ⊢ dom DProd = ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } )
49 48 eleq2i ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ dom DProd ↔ ⟨ 𝐺 , 𝑆 ⟩ ∈ ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) )
50 fveq2 ⊢ ( 𝑔 = 𝐺 → ( SubGrp ‘ 𝑔 ) = ( SubGrp ‘ 𝐺 ) )
51 50 feq3d ⊢ ( 𝑔 = 𝐺 → ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ↔ ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ) )
52 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Cntz ‘ 𝑔 ) = ( Cntz ‘ 𝐺 ) )
53 52 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Cntz ‘ 𝑔 ) = 𝑍 )
54 53 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) = ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) )
55 54 sseq2d ⊢ ( 𝑔 = 𝐺 → ( ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ↔ ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ) )
56 55 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ) )
57 50 fveq2d ⊢ ( 𝑔 = 𝐺 → ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) )
58 57 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) = 𝐾 )
59 58 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) )
60 59 ineq2d ⊢ ( 𝑔 = 𝐺 → ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) )
61 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
62 61 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = 0 )
63 62 sneqd ⊢ ( 𝑔 = 𝐺 → { ( 0g ‘ 𝑔 ) } = { 0 } )
64 60 63 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ↔ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) )
65 56 64 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ↔ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) )
66 65 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ↔ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) )
67 51 66 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) ↔ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
68 67 abbidv ⊢ ( 𝑔 = 𝐺 → { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } = { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } )
69 68 opeliunxp2 ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ ∪ 𝑔 ∈ Grp ( { 𝑔 } × { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ) )
70 37 49 69 3bitri ⊢ ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) } ) )
71 3anass ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
72 36 70 71 3bitr4g ⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )