Metamath Proof Explorer

Theorem grpolcan

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

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

Proof

Step Hyp Ref Expression
1 grplcan.1 ⊢ 𝑋 = ran 𝐺
2 oveq2 ⊢ ( ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
3 2 adantl ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
4 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
6 1 4 5 grpolinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐶 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) )
7 6 adantlr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) )
8 7 oveq1d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐴 ) = ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) )
9 1 5 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐶 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
10 9 adantrl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
11 simprr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
12 simprl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
13 10 11 12 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
14 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐴 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) )
15 13 14 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐴 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) )
16 15 anassrs ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐴 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) )
17 1 4 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) = 𝐴 )
18 17 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐴 ) = 𝐴 )
19 8 16 18 3eqtr3d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) = 𝐴 )
20 19 adantrl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) = 𝐴 )
21 20 adantr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐴 ) ) = 𝐴 )
22 6 adantrl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) = ( GId ‘ 𝐺 ) )
23 22 oveq1d ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐵 ) = ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) )
24 9 adantrl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
25 simprr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
26 simprl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
27 24 25 26 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
28 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐵 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
29 27 28 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 𝐶 ) 𝐺 𝐵 ) = ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
30 1 4 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) = 𝐵 )
31 30 adantrr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) = 𝐵 )
32 23 29 31 3eqtr3d ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) = 𝐵 )
33 32 adantlr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) = 𝐵 )
34 33 adantr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) 𝐺 ( 𝐶 𝐺 𝐵 ) ) = 𝐵 )
35 3 21 34 3eqtr3d ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) ) → 𝐴 = 𝐵 )
36 35 exp53 ⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐶 ∈ 𝑋 → ( ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) → 𝐴 = 𝐵 ) ) ) ) )
37 36 3imp2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) → 𝐴 = 𝐵 ) )
38 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) )
39 37 38 impbid1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 𝐺 𝐴 ) = ( 𝐶 𝐺 𝐵 ) ↔ 𝐴 = 𝐵 ) )