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 → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )