dsmmsubg

Description: The finite hull of a product of groups is additionally closed under negation and thus is a subgroup of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmsubg.p	$⊢ P = S ⨉_{𝑠} R$
	dsmmsubg.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
	dsmmsubg.i	$⊢ φ \to I \in W$
	dsmmsubg.s	$⊢ φ \to S \in V$
	dsmmsubg.r	$⊢ φ \to R : I ⟶ Grp$
Assertion	dsmmsubg	$⊢ φ \to H \in SubGrp (P)$

Proof

Step	Hyp	Ref	Expression
1		dsmmsubg.p	$⊢ P = S ⨉_{𝑠} R$
2		dsmmsubg.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
3		dsmmsubg.i	$⊢ φ \to I \in W$
4		dsmmsubg.s	$⊢ φ \to S \in V$
5		dsmmsubg.r	$⊢ φ \to R : I ⟶ Grp$
6		eqidd	$⊢ φ \to P ↾_{𝑠} H = P ↾_{𝑠} H$
7		eqidd	$⊢ φ \to 0_{P} = 0_{P}$
8		eqidd	$⊢ φ \to +_{P} = +_{P}$
9		fex	$⊢ (R : I ⟶ Grp \land I \in W) \to R \in V$
10	5 3 9	syl2anc	$⊢ φ \to R \in V$
11		eqid	$⊢ \{a \in {Base}_{(S ⨉_{𝑠} R)} \| \{b \in dom R \| a (b) \neq 0_{R (b)}\} \in Fin\} = \{a \in {Base}_{(S ⨉_{𝑠} R)} \| \{b \in dom R \| a (b) \neq 0_{R (b)}\} \in Fin\}$
12	11	dsmmbase	$⊢ R \in V \to \{a \in {Base}_{(S ⨉_{𝑠} R)} \| \{b \in dom R \| a (b) \neq 0_{R (b)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
13	10 12	syl	$⊢ φ \to \{a \in {Base}_{(S ⨉_{𝑠} R)} \| \{b \in dom R \| a (b) \neq 0_{R (b)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
14		ssrab2	$⊢ \{a \in {Base}_{(S ⨉_{𝑠} R)} \| \{b \in dom R \| a (b) \neq 0_{R (b)}\} \in Fin\} \subseteq {Base}_{(S ⨉_{𝑠} R)}$
15	13 14	eqsstrrdi	$⊢ φ \to {Base}_{(S \oplus_{m} R)} \subseteq {Base}_{(S ⨉_{𝑠} R)}$
16	1	fveq2i	$⊢ {Base}_{P} = {Base}_{(S ⨉_{𝑠} R)}$
17	15 2 16	3sstr4g	$⊢ φ \to H \subseteq {Base}_{P}$
18		grpmnd	$⊢ a \in Grp \to a \in Mnd$
19	18	ssriv	$⊢ Grp \subseteq Mnd$
20		fss	$⊢ (R : I ⟶ Grp \land Grp \subseteq Mnd) \to R : I ⟶ Mnd$
21	5 19 20	sylancl	$⊢ φ \to R : I ⟶ Mnd$
22		eqid	$⊢ 0_{P} = 0_{P}$
23	1 2 3 4 21 22	dsmm0cl	$⊢ φ \to 0_{P} \in H$
24	3	3ad2ant1	$⊢ (φ \land a \in H \land b \in H) \to I \in W$
25	4	3ad2ant1	$⊢ (φ \land a \in H \land b \in H) \to S \in V$
26	21	3ad2ant1	$⊢ (φ \land a \in H \land b \in H) \to R : I ⟶ Mnd$
27		simp2	$⊢ (φ \land a \in H \land b \in H) \to a \in H$
28		simp3	$⊢ (φ \land a \in H \land b \in H) \to b \in H$
29		eqid	$⊢ +_{P} = +_{P}$
30	1 2 24 25 26 27 28 29	dsmmacl	$⊢ (φ \land a \in H \land b \in H) \to a +_{P} b \in H$
31	1 3 4 5	prdsgrpd	$⊢ φ \to P \in Grp$
32	31	adantr	$⊢ (φ \land a \in H) \to P \in Grp$
33	17	sselda	$⊢ (φ \land a \in H) \to a \in {Base}_{P}$
34		eqid	$⊢ {Base}_{P} = {Base}_{P}$
35		eqid	$⊢ {inv}_{g} (P) = {inv}_{g} (P)$
36	34 35	grpinvcl	$⊢ (P \in Grp \land a \in {Base}_{P}) \to {inv}_{g} (P) (a) \in {Base}_{P}$
37	32 33 36	syl2anc	$⊢ (φ \land a \in H) \to {inv}_{g} (P) (a) \in {Base}_{P}$
38		simpr	$⊢ (φ \land a \in H) \to a \in H$
39		eqid	$⊢ S \oplus_{m} R = S \oplus_{m} R$
40	3	adantr	$⊢ (φ \land a \in H) \to I \in W$
41	5	ffnd	$⊢ φ \to R Fn I$
42	41	adantr	$⊢ (φ \land a \in H) \to R Fn I$
43	1 39 34 2 40 42	dsmmelbas	$⊢ (φ \land a \in H) \to (a \in H \leftrightarrow (a \in {Base}_{P} \land \{b \in I \| a (b) \neq 0_{R (b)}\} \in Fin))$
44	38 43	mpbid	$⊢ (φ \land a \in H) \to (a \in {Base}_{P} \land \{b \in I \| a (b) \neq 0_{R (b)}\} \in Fin)$
45	44	simprd	$⊢ (φ \land a \in H) \to \{b \in I \| a (b) \neq 0_{R (b)}\} \in Fin$
46	3	ad2antrr	$⊢ ((φ \land a \in H) \land b \in I) \to I \in W$
47	4	ad2antrr	$⊢ ((φ \land a \in H) \land b \in I) \to S \in V$
48	5	ad2antrr	$⊢ ((φ \land a \in H) \land b \in I) \to R : I ⟶ Grp$
49	33	adantr	$⊢ ((φ \land a \in H) \land b \in I) \to a \in {Base}_{P}$
50		simpr	$⊢ ((φ \land a \in H) \land b \in I) \to b \in I$
51	1 46 47 48 34 35 49 50	prdsinvgd2	$⊢ ((φ \land a \in H) \land b \in I) \to {inv}_{g} (P) (a) (b) = {inv}_{g} (R (b)) (a (b))$
52	51	adantrr	$⊢ ((φ \land a \in H) \land (b \in I \land a (b) = 0_{R (b)})) \to {inv}_{g} (P) (a) (b) = {inv}_{g} (R (b)) (a (b))$
53		fveq2	$⊢ a (b) = 0_{R (b)} \to {inv}_{g} (R (b)) (a (b)) = {inv}_{g} (R (b)) (0_{R (b)})$
54	53	ad2antll	$⊢ ((φ \land a \in H) \land (b \in I \land a (b) = 0_{R (b)})) \to {inv}_{g} (R (b)) (a (b)) = {inv}_{g} (R (b)) (0_{R (b)})$
55	5	ffvelrnda	$⊢ (φ \land b \in I) \to R (b) \in Grp$
56	55	adantlr	$⊢ ((φ \land a \in H) \land b \in I) \to R (b) \in Grp$
57		eqid	$⊢ 0_{R (b)} = 0_{R (b)}$
58		eqid	$⊢ {inv}_{g} (R (b)) = {inv}_{g} (R (b))$
59	57 58	grpinvid	$⊢ R (b) \in Grp \to {inv}_{g} (R (b)) (0_{R (b)}) = 0_{R (b)}$
60	56 59	syl	$⊢ ((φ \land a \in H) \land b \in I) \to {inv}_{g} (R (b)) (0_{R (b)}) = 0_{R (b)}$
61	60	adantrr	$⊢ ((φ \land a \in H) \land (b \in I \land a (b) = 0_{R (b)})) \to {inv}_{g} (R (b)) (0_{R (b)}) = 0_{R (b)}$
62	52 54 61	3eqtrd	$⊢ ((φ \land a \in H) \land (b \in I \land a (b) = 0_{R (b)})) \to {inv}_{g} (P) (a) (b) = 0_{R (b)}$
63	62	expr	$⊢ ((φ \land a \in H) \land b \in I) \to (a (b) = 0_{R (b)} \to {inv}_{g} (P) (a) (b) = 0_{R (b)})$
64	63	necon3d	$⊢ ((φ \land a \in H) \land b \in I) \to ({inv}_{g} (P) (a) (b) \neq 0_{R (b)} \to a (b) \neq 0_{R (b)})$
65	64	ss2rabdv	$⊢ (φ \land a \in H) \to \{b \in I \| {inv}_{g} (P) (a) (b) \neq 0_{R (b)}\} \subseteq \{b \in I \| a (b) \neq 0_{R (b)}\}$
66	45 65	ssfid	$⊢ (φ \land a \in H) \to \{b \in I \| {inv}_{g} (P) (a) (b) \neq 0_{R (b)}\} \in Fin$
67	1 39 34 2 40 42	dsmmelbas	$⊢ (φ \land a \in H) \to ({inv}_{g} (P) (a) \in H \leftrightarrow ({inv}_{g} (P) (a) \in {Base}_{P} \land \{b \in I \| {inv}_{g} (P) (a) (b) \neq 0_{R (b)}\} \in Fin))$
68	37 66 67	mpbir2and	$⊢ (φ \land a \in H) \to {inv}_{g} (P) (a) \in H$
69	6 7 8 17 23 30 68 31	issubgrpd2	$⊢ φ \to H \in SubGrp (P)$

Metamath Proof Explorer

Theorem dsmmsubg

Proof