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

Metamath Proof Explorer

Theorem subgdmdprd

Description: A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis subgdprd.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
Assertion subgdmdprd ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 subgdprd.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 reldmdprd ⊢ Rel dom DProd
3 2 brrelex2i ⊢ ( 𝐻 dom DProd 𝑆 → 𝑆 ∈ V )
4 3 a1i ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐻 dom DProd 𝑆 → 𝑆 ∈ V ) )
5 2 brrelex2i ⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
6 5 adantr ⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) → 𝑆 ∈ V )
7 6 a1i ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) → 𝑆 ∈ V ) )
8 ffvelcdm ⊢ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ 𝑥 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐻 ) )
9 8 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐻 ) )
10 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
11 10 subgss ⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐻 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( Base ‘ 𝐻 ) )
12 9 11 syl ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( Base ‘ 𝐻 ) )
13 1 subgbas ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 = ( Base ‘ 𝐻 ) )
14 13 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → 𝐴 = ( Base ‘ 𝐻 ) )
15 12 14 sseqtrrd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ 𝐴 )
16 15 biantrud ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( 𝑆 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
17 simpll ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
18 simplr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) )
19 eldifi ⊢ ( 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) → 𝑦 ∈ dom 𝑆 )
20 19 ad2antll ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → 𝑦 ∈ dom 𝑆 )
21 18 20 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐻 ) )
22 10 subgss ⊢ ( ( 𝑆 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐻 ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( Base ‘ 𝐻 ) )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( Base ‘ 𝐻 ) )
24 23 14 sseqtrrd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑆 ‘ 𝑦 ) ⊆ 𝐴 )
25 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
26 eqid ⊢ ( Cntz ‘ 𝐻 ) = ( Cntz ‘ 𝐻 )
27 1 25 26 resscntz ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑆 ‘ 𝑦 ) ⊆ 𝐴 ) → ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) = ( ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∩ 𝐴 ) )
28 17 24 27 syl2anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) = ( ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∩ 𝐴 ) )
29 28 sseq2d ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∩ 𝐴 ) ) )
30 ssin ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( 𝑆 ‘ 𝑥 ) ⊆ 𝐴 ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∩ 𝐴 ) )
31 29 30 bitr4di ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( 𝑆 ‘ 𝑥 ) ⊆ 𝐴 ) ) )
32 16 31 bitr4d ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ ( 𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
33 32 anassrs ⊢ ( ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) ∧ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ) → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
34 33 ralbidva ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
35 subgrcl ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
36 35 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → 𝐺 ∈ Grp )
37 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
38 37 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
39 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
40 36 38 39 3syl ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
41 1 subggrp ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
42 41 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → 𝐻 ∈ Grp )
43 10 subgacs ⊢ ( 𝐻 ∈ Grp → ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) )
44 acsmre ⊢ ( ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
45 42 43 44 3syl ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
46 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐻 ) )
47 imassrn ⊢ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ran 𝑆
48 frn ⊢ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) → ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) )
49 48 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) )
50 47 49 sstrid ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( SubGrp ‘ 𝐻 ) )
51 mresspw ⊢ ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) → ( SubGrp ‘ 𝐻 ) ⊆ 𝒫 ( Base ‘ 𝐻 ) )
52 45 51 syl ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( SubGrp ‘ 𝐻 ) ⊆ 𝒫 ( Base ‘ 𝐻 ) )
53 50 52 sstrd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐻 ) )
54 sspwuni ⊢ ( ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐻 ) ↔ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐻 ) )
55 53 54 sylib ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐻 ) )
56 45 46 55 mrcssidd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
57 46 mrccl ⊢ ( ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) ∧ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐻 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) )
58 45 55 57 syl2anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) )
59 1 subsubg ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 ) ) )
60 59 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 ) ) )
61 58 60 mpbid ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 ) )
62 61 simpld ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
63 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
64 63 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
65 40 56 62 64 syl3anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
66 13 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → 𝐴 = ( Base ‘ 𝐻 ) )
67 55 66 sseqtrrd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ 𝐴 )
68 37 subgss ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
69 68 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
70 67 69 sstrd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
71 40 63 70 mrcssidd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
72 63 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
73 40 70 72 syl2anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
74 simpll ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
75 63 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ 𝐴 ∧ 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 )
76 40 67 74 75 syl3anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 )
77 1 subsubg ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 ) ) )
78 77 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ 𝐴 ) ) )
79 73 76 78 mpbir2and ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) )
80 46 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) ∧ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
81 45 71 79 80 syl3anc ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
82 65 81 eqssd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) )
83 82 ineq2d ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) )
84 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
85 1 84 subg0 ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
86 85 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
87 86 sneqd ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → { ( 0g ‘ 𝐺 ) } = { ( 0g ‘ 𝐻 ) } )
88 83 87 eqeq12d ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ↔ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) )
89 34 88 anbi12d ⊢ ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) ∧ 𝑥 ∈ dom 𝑆 ) → ( ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ↔ ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) )
90 89 ralbidva ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ) → ( ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ↔ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) )
91 90 pm5.32da ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) )
92 1 subsubg ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝐴 ) ) )
93 elin ⊢ ( 𝑥 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) )
94 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
95 94 anbi2i ⊢ ( ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝐴 ) )
96 93 95 bitri ⊢ ( 𝑥 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝐴 ) )
97 92 96 bitr4di ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ↔ 𝑥 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) ) )
98 97 eqrdv ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( SubGrp ‘ 𝐻 ) = ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) )
99 98 sseq2d ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) ↔ ran 𝑆 ⊆ ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) ) )
100 ssin ⊢ ( ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ran 𝑆 ⊆ ( ( SubGrp ‘ 𝐺 ) ∩ 𝒫 𝐴 ) )
101 99 100 bitr4di ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) ↔ ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
102 101 anbi2d ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) ) ↔ ( 𝑆 Fn dom 𝑆 ∧ ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) ) )
103 df-f ⊢ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ ( SubGrp ‘ 𝐻 ) ) )
104 df-f ⊢ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ) )
105 104 anbi1i ⊢ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( ( 𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) )
106 anass ⊢ ( ( ( 𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( 𝑆 Fn dom 𝑆 ∧ ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
107 105 106 bitri ⊢ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( 𝑆 Fn dom 𝑆 ∧ ( ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
108 102 103 107 3bitr4g ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
109 108 anbi1d ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
110 91 109 bitr3d ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
111 110 adantr ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
112 dmexg ⊢ ( 𝑆 ∈ V → dom 𝑆 ∈ V )
113 112 adantl ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → dom 𝑆 ∈ V )
114 eqidd ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → dom 𝑆 = dom 𝑆 )
115 41 adantr ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → 𝐻 ∈ Grp )
116 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
117 26 116 46 dmdprd ⊢ ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐻 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) )
118 3anass ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ↔ ( 𝐻 ∈ Grp ∧ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) )
119 117 118 bitrdi ⊢ ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐻 ∈ Grp ∧ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) ) )
120 119 baibd ⊢ ( ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) ∧ 𝐻 ∈ Grp ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) )
121 113 114 115 120 syl21anc ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐻 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐻 ) } ) ) ) )
122 35 adantr ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → 𝐺 ∈ Grp )
123 25 84 63 dmdprd ⊢ ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
124 3anass ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
125 123 124 bitrdi ⊢ ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) ) )
126 125 baibd ⊢ ( ( ( dom 𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆 ) ∧ 𝐺 ∈ Grp ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
127 113 114 122 126 syl21anc ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
128 127 anbi1d ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
129 an32 ⊢ ( ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) )
130 128 129 bitrdi ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ↔ ( ( 𝑆 : dom 𝑆 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ∧ ∀ 𝑥 ∈ dom 𝑆 ( ∀ 𝑦 ∈ ( dom 𝑆 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( dom 𝑆 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
131 111 121 130 3bitr4d ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ V ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )
132 131 ex ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ V → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) ) )
133 4 7 132 pm5.21ndd ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐻 dom DProd 𝑆 ↔ ( 𝐺 dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴 ) ) )