Theorem 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	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
	dsmmsubg.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
	dsmmsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	dsmmsubg.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	dsmmsubg.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
Assertion	dsmmsubg	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		dsmmsubg.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2		dsmmsubg.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
3		dsmmsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		dsmmsubg.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5		dsmmsubg.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
6		eqidd	⊢ ( 𝜑 → ( 𝑃 ↾s 𝐻 ) = ( 𝑃 ↾s 𝐻 ) )
7		eqidd	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) )
8		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) )
9		fex	⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
10	5 3 9	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ V )
11		eqid	⊢ { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin }
12	11	dsmmbase	⊢ ( 𝑅 ∈ V → { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
13	10 12	syl	⊢ ( 𝜑 → { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
14		ssrab2	⊢ { 𝑎 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑏 ∈ dom 𝑅 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin } ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) )
15	13 14	eqsstrrdi	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
16	1	fveq2i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
17	15 2 16	3sstr4g	⊢ ( 𝜑 → 𝐻 ⊆ ( Base ‘ 𝑃 ) )
18		grpmnd	⊢ ( 𝑎 ∈ Grp → 𝑎 ∈ Mnd )
19	18	ssriv	⊢ Grp ⊆ Mnd
20		fss	⊢ ( ( 𝑅 : 𝐼 ⟶ Grp ∧ Grp ⊆ Mnd ) → 𝑅 : 𝐼 ⟶ Mnd )
21	5 19 20	sylancl	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
22		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
23	1 2 3 4 21 22	dsmm0cl	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐻 )
24	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝐼 ∈ 𝑊 )
25	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑆 ∈ 𝑉 )
26	21	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑅 : 𝐼 ⟶ Mnd )
27		simp2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑎 ∈ 𝐻 )
28		simp3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → 𝑏 ∈ 𝐻 )
29		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
30	1 2 24 25 26 27 28 29	dsmmacl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ∧ 𝑏 ∈ 𝐻 ) → ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝐻 )
31	1 3 4 5	prdsgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑃 ∈ Grp )
33	17	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ ( Base ‘ 𝑃 ) )
34		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
35		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
36	34 35	grpinvcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑃 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) )
37	32 33 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) )
38		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ 𝐻 )
39		eqid	⊢ ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 ⊕m 𝑅 )
40	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐼 ∈ 𝑊 )
41	5	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑅 Fn 𝐼 )
43	1 39 34 2 40 42	dsmmelbas	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑎 ∈ 𝐻 ↔ ( 𝑎 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) ) )
44	38 43	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑎 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) )
45	44	simprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin )
46	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
47	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
48	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑅 : 𝐼 ⟶ Grp )
49	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑃 ) )
50		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑏 ∈ 𝐼 )
51	1 46 47 48 34 35 49 50	prdsinvgd2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) )
52	51	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) )
53		fveq2	⊢ ( ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
54	53	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 𝑎 ‘ 𝑏 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
55	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑏 ) ∈ Grp )
56	55	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑏 ) ∈ Grp )
57		eqid	⊢ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) )
58		eqid	⊢ ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) = ( invg ‘ ( 𝑅 ‘ 𝑏 ) )
59	57 58	grpinvid	⊢ ( ( 𝑅 ‘ 𝑏 ) ∈ Grp → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) )
60	56 59	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) )
61	60	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑏 ) ) ‘ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) )
62	52 54 61	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑏 ∈ 𝐼 ∧ ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) )
63	62	expr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) = ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
64	63	necon3d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) → ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) ) )
65	64	ss2rabdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ⊆ { 𝑏 ∈ 𝐼 ∣ ( 𝑎 ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } )
66	45 65	ssfid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin )
67	1 39 34 2 40 42	dsmmelbas	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ 𝐻 ↔ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑏 ∈ 𝐼 ∣ ( ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ‘ 𝑏 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑏 ) ) } ∈ Fin ) ) )
68	37 66 67	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑎 ) ∈ 𝐻 )
69	6 7 8 17 23 30 68 31	issubgrpd2	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝑃 ) )