Metamath Proof Explorer

Theorem issubg3

Description: A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubg3.i ${⊢}{I}={inv}_{g}\left({G}\right)$
Assertion issubg3 ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$

Proof

Step Hyp Ref Expression
1 issubg3.i ${⊢}{I}={inv}_{g}\left({G}\right)$
2 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
3 2 subg0cl ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {0}_{{G}}\in {S}$
4 3 a1i ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)\to {0}_{{G}}\in {S}\right)$
5 2 subm0cl ${⊢}{S}\in \mathrm{SubMnd}\left({G}\right)\to {0}_{{G}}\in {S}$
6 5 adantr ${⊢}\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\to {0}_{{G}}\in {S}$
7 6 a1i ${⊢}{G}\in \mathrm{Grp}\to \left(\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\to {0}_{{G}}\in {S}\right)$
8 ne0i ${⊢}{0}_{{G}}\in {S}\to {S}\ne \varnothing$
9 id ${⊢}{0}_{{G}}\in {S}\to {0}_{{G}}\in {S}$
10 8 9 2thd ${⊢}{0}_{{G}}\in {S}\to \left({S}\ne \varnothing ↔{0}_{{G}}\in {S}\right)$
11 10 adantl ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left({S}\ne \varnothing ↔{0}_{{G}}\in {S}\right)$
12 r19.26 ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)↔\left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)$
13 12 a1i ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)↔\left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
14 11 13 3anbi23d ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {S}\ne \varnothing \wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)\right)↔\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)\right)$
15 anass ${⊢}\left(\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\right)\wedge \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
16 df-3an ${⊢}\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)$
17 16 anbi1i ${⊢}\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)↔\left(\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)$
18 df-3an ${⊢}\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\right)\wedge \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
19 15 17 18 3bitr4ri ${⊢}\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)$
20 14 19 syl6bb ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {S}\ne \varnothing \wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
21 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
22 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
23 21 22 1 issubg2 ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {S}\ne \varnothing \wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)\right)\right)$
24 23 adantr ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {S}\ne \varnothing \wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\wedge {I}\left({x}\right)\in {S}\right)\right)\right)$
25 grpmnd ${⊢}{G}\in \mathrm{Grp}\to {G}\in \mathrm{Mnd}$
26 21 2 22 issubm ${⊢}{G}\in \mathrm{Mnd}\to \left({S}\in \mathrm{SubMnd}\left({G}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\right)$
27 25 26 syl ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubMnd}\left({G}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\right)$
28 27 anbi1d ${⊢}{G}\in \mathrm{Grp}\to \left(\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
29 28 adantr ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left(\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)↔\left(\left({S}\subseteq {\mathrm{Base}}_{{G}}\wedge {0}_{{G}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{G}}{y}\in {S}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
30 20 24 29 3bitr4d ${⊢}\left({G}\in \mathrm{Grp}\wedge {0}_{{G}}\in {S}\right)\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$
31 30 ex ${⊢}{G}\in \mathrm{Grp}\to \left({0}_{{G}}\in {S}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)\right)$
32 4 7 31 pm5.21ndd ${⊢}{G}\in \mathrm{Grp}\to \left({S}\in \mathrm{SubGrp}\left({G}\right)↔\left({S}\in \mathrm{SubMnd}\left({G}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{I}\left({x}\right)\in {S}\right)\right)$