dprdspan

Description: The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016)

		Ref	Expression
	Hypothesis	dprdspan.k	$⊢ K = mrCls (SubGrp (G))$
	Assertion	dprdspan	$⊢ G dom DProd S \to G DProd S = K (⋃ ran S)$

Proof

Step	Hyp	Ref	Expression
1		dprdspan.k	$⊢ K = mrCls (SubGrp (G))$
2		id	$⊢ G dom DProd S \to G dom DProd S$
3		eqidd	$⊢ G dom DProd S \to dom S = dom S$
4		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	5	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
7		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
8	4 6 7	3syl	$⊢ G dom DProd S \to SubGrp (G) \in Moore ({Base}_{G})$
9		dprdf	$⊢ G dom DProd S \to S : dom S ⟶ SubGrp (G)$
10	9	ffnd	$⊢ G dom DProd S \to S Fn dom S$
11		fniunfv	$⊢ S Fn dom S \to ⋃_{k \in dom S} S (k) = ⋃ ran S$
12	10 11	syl	$⊢ G dom DProd S \to ⋃_{k \in dom S} S (k) = ⋃ ran S$
13		simpl	$⊢ (G dom DProd S \land k \in dom S) \to G dom DProd S$
14		eqidd	$⊢ (G dom DProd S \land k \in dom S) \to dom S = dom S$
15		simpr	$⊢ (G dom DProd S \land k \in dom S) \to k \in dom S$
16	13 14 15	dprdub	$⊢ (G dom DProd S \land k \in dom S) \to S (k) \subseteq G DProd S$
17	16	ralrimiva	$⊢ G dom DProd S \to \forall k \in dom S S (k) \subseteq G DProd S$
18		iunss	$⊢ ⋃_{k \in dom S} S (k) \subseteq G DProd S \leftrightarrow \forall k \in dom S S (k) \subseteq G DProd S$
19	17 18	sylibr	$⊢ G dom DProd S \to ⋃_{k \in dom S} S (k) \subseteq G DProd S$
20	12 19	eqsstrrd	$⊢ G dom DProd S \to ⋃ ran S \subseteq G DProd S$
21	5	dprdssv	$⊢ G DProd S \subseteq {Base}_{G}$
22	20 21	sstrdi	$⊢ G dom DProd S \to ⋃ ran S \subseteq {Base}_{G}$
23	1	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran S \subseteq {Base}_{G}) \to K (⋃ ran S) \in SubGrp (G)$
24	8 22 23	syl2anc	$⊢ G dom DProd S \to K (⋃ ran S) \in SubGrp (G)$
25		eqimss	$⊢ ⋃_{k \in dom S} S (k) = ⋃ ran S \to ⋃_{k \in dom S} S (k) \subseteq ⋃ ran S$
26	12 25	syl	$⊢ G dom DProd S \to ⋃_{k \in dom S} S (k) \subseteq ⋃ ran S$
27		iunss	$⊢ ⋃_{k \in dom S} S (k) \subseteq ⋃ ran S \leftrightarrow \forall k \in dom S S (k) \subseteq ⋃ ran S$
28	26 27	sylib	$⊢ G dom DProd S \to \forall k \in dom S S (k) \subseteq ⋃ ran S$
29	28	r19.21bi	$⊢ (G dom DProd S \land k \in dom S) \to S (k) \subseteq ⋃ ran S$
30	8 1 22	mrcssidd	$⊢ G dom DProd S \to ⋃ ran S \subseteq K (⋃ ran S)$
31	30	adantr	$⊢ (G dom DProd S \land k \in dom S) \to ⋃ ran S \subseteq K (⋃ ran S)$
32	29 31	sstrd	$⊢ (G dom DProd S \land k \in dom S) \to S (k) \subseteq K (⋃ ran S)$
33	2 3 24 32	dprdlub	$⊢ G dom DProd S \to G DProd S \subseteq K (⋃ ran S)$
34		dprdsubg	$⊢ G dom DProd S \to G DProd S \in SubGrp (G)$
35	1	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran S \subseteq G DProd S \land G DProd S \in SubGrp (G)) \to K (⋃ ran S) \subseteq G DProd S$
36	8 20 34 35	syl3anc	$⊢ G dom DProd S \to K (⋃ ran S) \subseteq G DProd S$
37	33 36	eqssd	$⊢ G dom DProd S \to G DProd S = K (⋃ ran S)$

Metamath Proof Explorer

Theorem dprdspan

Proof