This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dprdsubg

Description: The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdsubg ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2 1 dprdssv ⊢ ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 )
3 2 a1i ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 eqid ⊢ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
6 id ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 dom DProd 𝑆 )
7 eqidd ⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 = dom 𝑆 )
8 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
9 fnconstg ⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) Fn dom 𝑆 )
10 8 9 mp1i ⊢ ( 𝐺 dom DProd 𝑆 → ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) Fn dom 𝑆 )
11 8 fvconst2 ⊢ ( 𝑘 ∈ dom 𝑆 → ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ‘ 𝑘 ) = ( 0g ‘ 𝐺 ) )
12 11 adantl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ‘ 𝑘 ) = ( 0g ‘ 𝐺 ) )
13 dprdf ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) )
14 13 ffvelcdmda ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
15 4 subg0cl ⊢ ( ( 𝑆 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑆 ‘ 𝑘 ) )
16 14 15 syl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑆 ‘ 𝑘 ) )
17 12 16 eqeltrd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑘 ∈ dom 𝑆 ) → ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
18 17 ralrimiva ⊢ ( 𝐺 dom DProd 𝑆 → ∀ 𝑘 ∈ dom 𝑆 ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
19 df-nel ⊢ ( dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V )
20 dprddomprc ⊢ ( dom 𝑆 ∉ V → ¬ 𝐺 dom DProd 𝑆 )
21 19 20 sylbir ⊢ ( ¬ dom 𝑆 ∈ V → ¬ 𝐺 dom DProd 𝑆 )
22 21 con4i ⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
23 8 a1i ⊢ ( 𝐺 dom DProd 𝑆 → ( 0g ‘ 𝐺 ) ∈ V )
24 22 23 fczfsuppd ⊢ ( 𝐺 dom DProd 𝑆 → ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) finSupp ( 0g ‘ 𝐺 ) )
25 5 6 7 dprdw ⊢ ( 𝐺 dom DProd 𝑆 → ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↔ ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) Fn dom 𝑆 ∧ ∀ 𝑘 ∈ dom 𝑆 ( ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) ∧ ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) finSupp ( 0g ‘ 𝐺 ) ) ) )
26 10 18 24 25 mpbir3and ⊢ ( 𝐺 dom DProd 𝑆 → ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
27 4 5 6 7 26 eldprdi ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 Σg ( dom 𝑆 × { ( 0g ‘ 𝐺 ) } ) ) ∈ ( 𝐺 DProd 𝑆 ) )
28 27 ne0d ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ≠ ∅ )
29 eqid ⊢ dom 𝑆 = dom 𝑆
30 4 5 eldprd ⊢ ( dom 𝑆 = dom 𝑆 → ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) ) )
31 30 baibd ⊢ ( ( dom 𝑆 = dom 𝑆 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) )
32 4 5 eldprd ⊢ ( dom 𝑆 = dom 𝑆 → ( 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) ) )
33 32 baibd ⊢ ( ( dom 𝑆 = dom 𝑆 ∧ 𝐺 dom DProd 𝑆 ) → ( 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ↔ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) )
34 31 33 anbi12d ⊢ ( ( dom 𝑆 = dom 𝑆 ∧ 𝐺 dom DProd 𝑆 ) → ( ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∧ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ) ↔ ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) ) )
35 29 34 mpan ⊢ ( 𝐺 dom DProd 𝑆 → ( ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∧ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ) ↔ ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) ) )
36 reeanv ⊢ ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ( 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ 𝑦 = ( 𝐺 Σg 𝑔 ) ) ↔ ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) )
37 simpl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → 𝐺 dom DProd 𝑆 )
38 eqidd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → dom 𝑆 = dom 𝑆 )
39 simprl ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
40 simprr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
41 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
42 4 5 37 38 39 40 41 dprdfsub ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( ( 𝑓 ∘f ( -g ‘ 𝐺 ) 𝑔 ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ ( 𝐺 Σg ( 𝑓 ∘f ( -g ‘ 𝐺 ) 𝑔 ) ) = ( ( 𝐺 Σg 𝑓 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝑔 ) ) ) )
43 42 simprd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( 𝐺 Σg ( 𝑓 ∘f ( -g ‘ 𝐺 ) 𝑔 ) ) = ( ( 𝐺 Σg 𝑓 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝑔 ) ) )
44 42 simpld ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( 𝑓 ∘f ( -g ‘ 𝐺 ) 𝑔 ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
45 4 5 37 38 44 eldprdi ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( 𝐺 Σg ( 𝑓 ∘f ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( 𝐺 DProd 𝑆 ) )
46 43 45 eqeltrrd ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( ( 𝐺 Σg 𝑓 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝑔 ) ) ∈ ( 𝐺 DProd 𝑆 ) )
47 oveq12 ⊢ ( ( 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ 𝑦 = ( 𝐺 Σg 𝑔 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( ( 𝐺 Σg 𝑓 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝑔 ) ) )
48 47 eleq1d ⊢ ( ( 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ 𝑦 = ( 𝐺 Σg 𝑔 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( ( 𝐺 Σg 𝑓 ) ( -g ‘ 𝐺 ) ( 𝐺 Σg 𝑔 ) ) ∈ ( 𝐺 DProd 𝑆 ) ) )
49 46 48 syl5ibrcom ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∧ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ) → ( ( 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ 𝑦 = ( 𝐺 Σg 𝑔 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) )
50 49 rexlimdvva ⊢ ( 𝐺 dom DProd 𝑆 → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ( 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ 𝑦 = ( 𝐺 Σg 𝑔 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) )
51 36 50 biimtrrid ⊢ ( 𝐺 dom DProd 𝑆 → ( ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ∧ ∃ 𝑔 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑦 = ( 𝐺 Σg 𝑔 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) )
52 35 51 sylbid ⊢ ( 𝐺 dom DProd 𝑆 → ( ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∧ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) )
53 52 ralrimivv ⊢ ( 𝐺 dom DProd 𝑆 → ∀ 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∀ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) )
54 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
55 1 41 issubg4 ⊢ ( 𝐺 ∈ Grp → ( ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 DProd 𝑆 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∀ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) ) )
56 54 55 syl ⊢ ( 𝐺 dom DProd 𝑆 → ( ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( 𝐺 DProd 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 DProd 𝑆 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ∀ 𝑦 ∈ ( 𝐺 DProd 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝐺 DProd 𝑆 ) ) ) )
57 3 28 53 56 mpbir3and ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )