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 ${⊢}{P}={S}{⨉}_{𝑠}{R}$
dsmmsubg.h ${⊢}{H}={\mathrm{Base}}_{\left({S}{\oplus }_{m}{R}\right)}$
dsmmsubg.i ${⊢}{\phi }\to {I}\in {W}$
dsmmsubg.s ${⊢}{\phi }\to {S}\in {V}$
dsmmsubg.r ${⊢}{\phi }\to {R}:{I}⟶\mathrm{Grp}$
Assertion dsmmsubg ${⊢}{\phi }\to {H}\in \mathrm{SubGrp}\left({P}\right)$

Proof

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