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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) = ( 𝐵 𝐺 𝐶 ) ↔ 𝐴 = 𝐵 ) )