# Metamath Proof Explorer

## Theorem grpoidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpoidval.1 ${⊢}{X}=\mathrm{ran}{G}$
grpoidval.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
Assertion grpoidinv2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$

### Proof

Step Hyp Ref Expression
1 grpoidval.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpoidval.2 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
3 1 2 grpoidval ${⊢}{G}\in \mathrm{GrpOp}\to {U}=\left(\iota {u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)$
4 1 grpoideu ${⊢}{G}\in \mathrm{GrpOp}\to \exists !{u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}$
5 riotacl2 ${⊢}\exists !{u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\to \left(\iota {u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)\in \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right\}$
6 4 5 syl ${⊢}{G}\in \mathrm{GrpOp}\to \left(\iota {u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)\in \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right\}$
7 3 6 eqeltrd ${⊢}{G}\in \mathrm{GrpOp}\to {U}\in \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right\}$
8 simpll ${⊢}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to {u}{G}{x}={x}$
9 8 ralimi ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}$
10 9 rgenw ${⊢}\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)$
11 10 a1i ${⊢}{G}\in \mathrm{GrpOp}\to \forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)$
12 1 grpoidinv ${⊢}{G}\in \mathrm{GrpOp}\to \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)$
13 11 12 4 3jca ${⊢}{G}\in \mathrm{GrpOp}\to \left(\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\wedge \exists !{u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)$
14 reupick2 ${⊢}\left(\left(\forall {u}\in {X}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\wedge \exists !{u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right)\wedge {u}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\right)$
15 13 14 sylan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {u}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\right)$
16 15 rabbidva ${⊢}{G}\in \mathrm{GrpOp}\to \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}{G}{x}={x}\right\}=\left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\right\}$
17 7 16 eleqtrd ${⊢}{G}\in \mathrm{GrpOp}\to {U}\in \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\right\}$
18 oveq1 ${⊢}{u}={U}\to {u}{G}{x}={U}{G}{x}$
19 18 eqeq1d ${⊢}{u}={U}\to \left({u}{G}{x}={x}↔{U}{G}{x}={x}\right)$
20 oveq2 ${⊢}{u}={U}\to {x}{G}{u}={x}{G}{U}$
21 20 eqeq1d ${⊢}{u}={U}\to \left({x}{G}{u}={x}↔{x}{G}{U}={x}\right)$
22 19 21 anbi12d ${⊢}{u}={U}\to \left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)↔\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\right)$
23 eqeq2 ${⊢}{u}={U}\to \left({y}{G}{x}={u}↔{y}{G}{x}={U}\right)$
24 eqeq2 ${⊢}{u}={U}\to \left({x}{G}{y}={u}↔{x}{G}{y}={U}\right)$
25 23 24 anbi12d ${⊢}{u}={U}\to \left(\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)↔\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)$
26 25 rexbidv ${⊢}{u}={U}\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)$
27 22 26 anbi12d ${⊢}{u}={U}\to \left(\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)↔\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)\right)$
28 27 ralbidv ${⊢}{u}={U}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)\right)$
29 28 elrab ${⊢}{U}\in \left\{{u}\in {X}|\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={u}\wedge {x}{G}{y}={u}\right)\right)\right\}↔\left({U}\in {X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)\right)$
30 17 29 sylib ${⊢}{G}\in \mathrm{GrpOp}\to \left({U}\in {X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)\right)$
31 30 simprd ${⊢}{G}\in \mathrm{GrpOp}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)$
32 oveq2 ${⊢}{x}={A}\to {U}{G}{x}={U}{G}{A}$
33 id ${⊢}{x}={A}\to {x}={A}$
34 32 33 eqeq12d ${⊢}{x}={A}\to \left({U}{G}{x}={x}↔{U}{G}{A}={A}\right)$
35 oveq1 ${⊢}{x}={A}\to {x}{G}{U}={A}{G}{U}$
36 35 33 eqeq12d ${⊢}{x}={A}\to \left({x}{G}{U}={x}↔{A}{G}{U}={A}\right)$
37 34 36 anbi12d ${⊢}{x}={A}\to \left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)↔\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\right)$
38 oveq2 ${⊢}{x}={A}\to {y}{G}{x}={y}{G}{A}$
39 38 eqeq1d ${⊢}{x}={A}\to \left({y}{G}{x}={U}↔{y}{G}{A}={U}\right)$
40 oveq1 ${⊢}{x}={A}\to {x}{G}{y}={A}{G}{y}$
41 40 eqeq1d ${⊢}{x}={A}\to \left({x}{G}{y}={U}↔{A}{G}{y}={U}\right)$
42 39 41 anbi12d ${⊢}{x}={A}\to \left(\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)↔\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
43 42 rexbidv ${⊢}{x}={A}\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)↔\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
44 37 43 anbi12d ${⊢}{x}={A}\to \left(\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)↔\left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)\right)$
45 44 rspccva ${⊢}\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({U}{G}{x}={x}\wedge {x}{G}{U}={x}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{x}={U}\wedge {x}{G}{y}={U}\right)\right)\wedge {A}\in {X}\right)\to \left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$
46 31 45 sylan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to \left(\left({U}{G}{A}={A}\wedge {A}{G}{U}={A}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{A}={U}\wedge {A}{G}{y}={U}\right)\right)$