# Metamath Proof Explorer

## Theorem grpoidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 𝑋 = ran 𝐺
Assertion grpoidinv ( 𝐺 ∈ GrpOp → ∃ 𝑢𝑋𝑥𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )

### Proof

Step Hyp Ref Expression
1 grpfo.1 𝑋 = ran 𝐺
2 simpl ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) → ( 𝑢 𝐺 𝑧 ) = 𝑧 )
3 2 ralimi ( ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) → ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 )
4 oveq2 ( 𝑧 = 𝑥 → ( 𝑢 𝐺 𝑧 ) = ( 𝑢 𝐺 𝑥 ) )
5 id ( 𝑧 = 𝑥𝑧 = 𝑥 )
6 4 5 eqeq12d ( 𝑧 = 𝑥 → ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ↔ ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
7 6 rspccva ( ( ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧𝑥𝑋 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
8 3 7 sylan ( ( ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ∧ 𝑥𝑋 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
9 8 adantll ( ( ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ∧ 𝑥𝑋 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
10 9 adantll ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
11 simpl ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) → 𝐺 ∈ GrpOp )
12 11 anim1i ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( 𝐺 ∈ GrpOp ∧ 𝑥𝑋 ) )
13 id ( ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) → ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) )
14 13 adantrr ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) → ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) )
15 14 adantr ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) )
16 3 adantl ( ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) → ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 )
17 16 ad2antlr ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 )
18 simpr ( ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) → ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 )
19 18 ralimi ( ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) → ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 )
20 19 adantl ( ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) → ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 )
21 20 ad2antlr ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 )
22 15 17 21 jca32 ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) ∧ ( ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) )
23 biid ( ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 ↔ ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 )
24 biid ( ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ↔ ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 )
25 1 23 24 grpoidinvlem3 ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝑢𝑋 ) ∧ ( ∀ 𝑧𝑋 ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∀ 𝑧𝑋𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ∧ 𝑥𝑋 ) → ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) )
26 22 25 sylancom ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) )
27 1 grpoidinvlem4 ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥𝑋 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ( 𝑥 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑥 ) )
28 12 26 27 syl2anc ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑥 𝐺 𝑢 ) = ( 𝑢 𝐺 𝑥 ) )
29 28 10 eqtrd ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑥 𝐺 𝑢 ) = 𝑥 )
30 10 29 26 jca31 ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) ∧ 𝑥𝑋 ) → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )
31 30 ralrimiva ( ( 𝐺 ∈ GrpOp ∧ ( 𝑢𝑋 ∧ ∀ 𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) ) ) → ∀ 𝑥𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )
32 1 grpolidinv ( 𝐺 ∈ GrpOp → ∃ 𝑢𝑋𝑧𝑋 ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ∧ ∃ 𝑤𝑋 ( 𝑤 𝐺 𝑧 ) = 𝑢 ) )
33 31 32 reximddv ( 𝐺 ∈ GrpOp → ∃ 𝑢𝑋𝑥𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )