This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpoid

Description: Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpoinveu.1 ⊢ 𝑋 = ran 𝐺
grpoinveu.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion grpoid ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 𝑈 ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 grpoinveu.1 ⊢ 𝑋 = ran 𝐺
2 grpoinveu.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 1 2 grpoidcl ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋 )
4 1 grporcan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) )
5 4 3exp2 ⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( 𝑈 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) ) ) )
6 3 5 mpid ⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) ) )
7 6 pm2.43d ⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) ) )
8 7 imp ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ 𝐴 = 𝑈 ) )
9 1 2 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐺 𝐴 ) = 𝐴 )
10 9 eqeq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )
11 8 10 bitr3d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 𝑈 ↔ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) )