subgdmdprd

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

		Ref	Expression
	Hypothesis	subgdprd.1	$⊢ H = G ↾_{𝑠} A$
	Assertion	subgdmdprd	$⊢ A \in SubGrp (G) \to (H dom DProd S \leftrightarrow (G dom DProd S \land ran S \subseteq 𝒫 A))$

Proof

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

Metamath Proof Explorer

Theorem subgdmdprd

Proof