This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑃 ) )