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

Metamath Proof Explorer

Theorem dsmmsubg

Proof