# Metamath Proof Explorer

## Theorem grporcan

Description: Right cancellation law for groups. (Contributed by NM, 26-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grprcan.1 𝑋 = ran 𝐺
Assertion grporcan ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ↔ 𝐴 = 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 grprcan.1 𝑋 = ran 𝐺
2 eqid ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
3 1 2 grpoidinv2 ( ( 𝐺 ∈ GrpOp ∧ 𝐶𝑋 ) → ( ( ( ( GId ‘ 𝐺 ) 𝐺 𝐶 ) = 𝐶 ∧ ( 𝐶 𝐺 ( GId ‘ 𝐺 ) ) = 𝐶 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ) ) )
4 simpr ( ( ( 𝑦 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ) → ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) )
5 4 reximi ( ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ) → ∃ 𝑦𝑋 ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) )
6 5 adantl ( ( ( ( ( GId ‘ 𝐺 ) 𝐺 𝐶 ) = 𝐶 ∧ ( 𝐶 𝐺 ( GId ‘ 𝐺 ) ) = 𝐶 ) ∧ ∃ 𝑦𝑋 ( ( 𝑦 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ) ) → ∃ 𝑦𝑋 ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) )
7 3 6 syl ( ( 𝐺 ∈ GrpOp ∧ 𝐶𝑋 ) → ∃ 𝑦𝑋 ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) )
8 7 ad2ant2rl ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ∃ 𝑦𝑋 ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) )
9 oveq1 ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) )
10 9 ad2antll ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) )
11 1 grpoass ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴𝑋𝐶𝑋𝑦𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
12 11 3anassrs ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ 𝐶𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
13 12 adantlrl ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ 𝑦𝑋 ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
14 13 adantrr ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
15 1 grpoass ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵𝑋𝐶𝑋𝑦𝑋 ) ) → ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
16 15 3exp2 ( 𝐺 ∈ GrpOp → ( 𝐵𝑋 → ( 𝐶𝑋 → ( 𝑦𝑋 → ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) ) ) ) )
17 16 imp42 ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ 𝑦𝑋 ) → ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
18 17 adantllr ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ 𝑦𝑋 ) → ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
19 18 adantrr ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( ( 𝐵 𝐺 𝐶 ) 𝐺 𝑦 ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
20 10 14 19 3eqtr3d ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
21 20 adantrrl ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) )
22 oveq2 ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) → ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
23 22 ad2antrl ( ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
24 23 adantl ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐴 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
25 oveq2 ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) → ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) )
26 25 ad2antrl ( ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) → ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) )
27 26 adantl ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐵 𝐺 ( 𝐶 𝐺 𝑦 ) ) = ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) )
28 21 24 27 3eqtr3d ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) )
29 1 2 grporid ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
30 29 ad2antrr ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
31 1 2 grporid ( ( 𝐺 ∈ GrpOp ∧ 𝐵𝑋 ) → ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) = 𝐵 )
32 31 ad2ant2r ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) = 𝐵 )
33 32 adantr ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → ( 𝐵 𝐺 ( GId ‘ 𝐺 ) ) = 𝐵 )
34 28 30 33 3eqtr3d ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) ∧ ( 𝑦𝑋 ∧ ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) ∧ ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ) ) ) → 𝐴 = 𝐵 )
35 34 exp45 ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( 𝑦𝑋 → ( ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) → 𝐴 = 𝐵 ) ) ) )
36 35 rexlimdv ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ∃ 𝑦𝑋 ( 𝐶 𝐺 𝑦 ) = ( GId ‘ 𝐺 ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) → 𝐴 = 𝐵 ) ) )
37 8 36 mpd ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) → 𝐴 = 𝐵 ) )
38 oveq1 ( 𝐴 = 𝐵 → ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) )
39 37 38 impbid1 ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) ∧ ( 𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ↔ 𝐴 = 𝐵 ) )
40 39 exp43 ( 𝐺 ∈ GrpOp → ( 𝐴𝑋 → ( 𝐵𝑋 → ( 𝐶𝑋 → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ↔ 𝐴 = 𝐵 ) ) ) ) )
41 40 3imp2 ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ↔ 𝐴 = 𝐵 ) )