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