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	$⊢ Z = Cntz (G)$
	dmdprd.0	$⊢ \underset{˙}{0} = 0_{G}$
	dmdprd.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	dmdprd	$⊢ (I \in V \land dom S = I) \to (G dom DProd S \leftrightarrow (G \in Grp \land S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$

Proof

Step	Hyp	Ref	Expression
1		dmdprd.z	$⊢ Z = Cntz (G)$
2		dmdprd.0	$⊢ \underset{˙}{0} = 0_{G}$
3		dmdprd.k	$⊢ K = mrCls (SubGrp (G))$
4		elex	$⊢ S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\} \to S \in V$
5	4	a1i	$⊢ (I \in V \land dom S = I) \to (S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\} \to S \in V)$
6		fex	$⊢ (S : I ⟶ SubGrp (G) \land I \in V) \to S \in V$
7	6	expcom	$⊢ I \in V \to (S : I ⟶ SubGrp (G) \to S \in V)$
8	7	adantr	$⊢ (I \in V \land dom S = I) \to (S : I ⟶ SubGrp (G) \to S \in V)$
9	8	adantrd	$⊢ (I \in V \land dom S = I) \to ((S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})) \to S \in V)$
10		df-sbc	$⊢ \underset{˙}{[} S / h \underset{˙}{]} (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})) \leftrightarrow S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\}$
11		simpr	$⊢ ((I \in V \land dom S = I) \land S \in V) \to S \in V$
12		simpr	$⊢ ((I \in V \land dom S = I) \land h = S) \to h = S$
13	12	dmeqd	$⊢ ((I \in V \land dom S = I) \land h = S) \to dom h = dom S$
14		simplr	$⊢ ((I \in V \land dom S = I) \land h = S) \to dom S = I$
15	13 14	eqtrd	$⊢ ((I \in V \land dom S = I) \land h = S) \to dom h = I$
16	12 15	feq12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to (h : dom h ⟶ SubGrp (G) \leftrightarrow S : I ⟶ SubGrp (G))$
17	15	difeq1d	$⊢ ((I \in V \land dom S = I) \land h = S) \to dom h ∖ \{x\} = I ∖ \{x\}$
18	12	fveq1d	$⊢ ((I \in V \land dom S = I) \land h = S) \to h (x) = S (x)$
19	12	fveq1d	$⊢ ((I \in V \land dom S = I) \land h = S) \to h (y) = S (y)$
20	19	fveq2d	$⊢ ((I \in V \land dom S = I) \land h = S) \to Z (h (y)) = Z (S (y))$
21	18 20	sseq12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to (h (x) \subseteq Z (h (y)) \leftrightarrow S (x) \subseteq Z (S (y)))$
22	17 21	raleqbidv	$⊢ ((I \in V \land dom S = I) \land h = S) \to (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \leftrightarrow \forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)))$
23	12 17	imaeq12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to h [dom h ∖ \{x\}] = S [I ∖ \{x\}]$
24	23	unieqd	$⊢ ((I \in V \land dom S = I) \land h = S) \to ⋃ h [dom h ∖ \{x\}] = ⋃ S [I ∖ \{x\}]$
25	24	fveq2d	$⊢ ((I \in V \land dom S = I) \land h = S) \to K (⋃ h [dom h ∖ \{x\}]) = K (⋃ S [I ∖ \{x\}])$
26	18 25	ineq12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = S (x) \cap K (⋃ S [I ∖ \{x\}])$
27	26	eqeq1d	$⊢ ((I \in V \land dom S = I) \land h = S) \to (h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\} \leftrightarrow S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})$
28	22 27	anbi12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to ((\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}) \leftrightarrow (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\}))$
29	15 28	raleqbidv	$⊢ ((I \in V \land dom S = I) \land h = S) \to (\forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}) \leftrightarrow \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\}))$
30	16 29	anbi12d	$⊢ ((I \in V \land dom S = I) \land h = S) \to ((h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})) \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
31	30	adantlr	$⊢ (((I \in V \land dom S = I) \land S \in V) \land h = S) \to ((h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})) \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
32	11 31	sbcied	$⊢ ((I \in V \land dom S = I) \land S \in V) \to (\underset{˙}{[} S / h \underset{˙}{]} (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})) \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
33	10 32	bitr3id	$⊢ ((I \in V \land dom S = I) \land S \in V) \to (S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\} \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
34	33	ex	$⊢ (I \in V \land dom S = I) \to (S \in V \to (S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\} \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\}))))$
35	5 9 34	pm5.21ndd	$⊢ (I \in V \land dom S = I) \to (S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\} \leftrightarrow (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
36	35	anbi2d	$⊢ (I \in V \land dom S = I) \to ((G \in Grp \land S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\}) \leftrightarrow (G \in Grp \land (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\}))))$
37		df-br	$⊢ G dom DProd S \leftrightarrow ⟨G, S⟩ \in dom DProd$
38		fvex	$⊢ s (x) \in V$
39	38	rgenw	$⊢ \forall x \in dom s s (x) \in V$
40		ixpexg	$⊢ \forall x \in dom s s (x) \in V \to \underset{x \in dom s}{⨉} s (x) \in V$
41	39 40	ax-mp	$⊢ \underset{x \in dom s}{⨉} s (x) \in V$
42	41	mptrabex	$⊢ (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
43	42	rnex	$⊢ ran (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
44	43	rgen2w	$⊢ \forall g \in Grp \forall s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\} ran (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
45		df-dprd	$⊢ DProd = (g \in Grp, s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\} ⟼ ran (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f))$
46	45	fmpox	$⊢ \forall g \in Grp \forall s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\} ran (f \in \{h \in \underset{x \in dom s}{⨉} s (x) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V \leftrightarrow DProd : ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\}) ⟶ V$
47	44 46	mpbi	$⊢ DProd : ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\}) ⟶ V$
48	47	fdmi	$⊢ dom DProd = ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\})$
49	48	eleq2i	$⊢ ⟨G, S⟩ \in dom DProd \leftrightarrow ⟨G, S⟩ \in ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\})$
50		fveq2	$⊢ g = G \to SubGrp (g) = SubGrp (G)$
51	50	feq3d	$⊢ g = G \to (h : dom h ⟶ SubGrp (g) \leftrightarrow h : dom h ⟶ SubGrp (G))$
52		fveq2	$⊢ g = G \to Cntz (g) = Cntz (G)$
53	52 1	eqtr4di	$⊢ g = G \to Cntz (g) = Z$
54	53	fveq1d	$⊢ g = G \to Cntz (g) (h (y)) = Z (h (y))$
55	54	sseq2d	$⊢ g = G \to (h (x) \subseteq Cntz (g) (h (y)) \leftrightarrow h (x) \subseteq Z (h (y)))$
56	55	ralbidv	$⊢ g = G \to (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \leftrightarrow \forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)))$
57	50	fveq2d	$⊢ g = G \to mrCls (SubGrp (g)) = mrCls (SubGrp (G))$
58	57 3	eqtr4di	$⊢ g = G \to mrCls (SubGrp (g)) = K$
59	58	fveq1d	$⊢ g = G \to mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = K (⋃ h [dom h ∖ \{x\}])$
60	59	ineq2d	$⊢ g = G \to h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = h (x) \cap K (⋃ h [dom h ∖ \{x\}])$
61		fveq2	$⊢ g = G \to 0_{g} = 0_{G}$
62	61 2	eqtr4di	$⊢ g = G \to 0_{g} = \underset{˙}{0}$
63	62	sneqd	$⊢ g = G \to \{0_{g}\} = \{\underset{˙}{0}\}$
64	60 63	eqeq12d	$⊢ g = G \to (h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\} \leftrightarrow h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})$
65	56 64	anbi12d	$⊢ g = G \to ((\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}) \leftrightarrow (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))$
66	65	ralbidv	$⊢ g = G \to (\forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}) \leftrightarrow \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))$
67	51 66	anbi12d	$⊢ g = G \to ((h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\})) \leftrightarrow (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\})))$
68	67	abbidv	$⊢ g = G \to \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\} = \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\}$
69	68	opeliunxp2	$⊢ ⟨G, S⟩ \in ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Cntz (g) (h (y)) \land h (x) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{x\}]) = \{0_{g}\}))\}) \leftrightarrow (G \in Grp \land S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\})$
70	37 49 69	3bitri	$⊢ G dom DProd S \leftrightarrow (G \in Grp \land S \in \{h \| (h : dom h ⟶ SubGrp (G) \land \forall x \in dom h (\forall y \in (dom h ∖ \{x\}) h (x) \subseteq Z (h (y)) \land h (x) \cap K (⋃ h [dom h ∖ \{x\}]) = \{\underset{˙}{0}\}))\})$
71		3anass	$⊢ (G \in Grp \land S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})) \leftrightarrow (G \in Grp \land (S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
72	36 70 71	3bitr4g	$⊢ (I \in V \land dom S = I) \to (G dom DProd S \leftrightarrow (G \in Grp \land S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$

Metamath Proof Explorer

Theorem dmdprd

Proof