Metamath Proof Explorer

Theorem grplcan

Description: Left cancellation law for groups. (Contributed by NM, 25-Aug-2011)

Ref Expression
Hypotheses grplcan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grplcan.p ⊢ + = ( +g ‘ 𝐺 )
Assertion grplcan ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 grplcan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grplcan.p ⊢ + = ( +g ‘ 𝐺 )
3 oveq2 ⊢ ( ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
4 3 adantl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
7 1 2 5 6 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) = ( 0g ‘ 𝐺 ) )
8 7 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) = ( 0g ‘ 𝐺 ) )
9 8 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( 0g ‘ 𝐺 ) + 𝑋 ) )
10 1 6 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
11 10 adantrl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
12 simprr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
13 simprl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
14 11 12 13 3jca ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
15 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) )
16 14 15 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) )
17 16 anassrs ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑋 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) )
18 1 2 5 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
19 18 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
20 9 17 19 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = 𝑋 )
21 20 adantrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = 𝑋 )
22 21 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑋 ) ) = 𝑋 )
23 7 adantrl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) = ( 0g ‘ 𝐺 ) )
24 23 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( 0g ‘ 𝐺 ) + 𝑌 ) )
25 10 adantrl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 )
26 simprr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
27 simprl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
28 25 26 27 3jca ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
29 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
30 28 29 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + 𝑍 ) + 𝑌 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) )
31 1 2 5 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
32 31 adantrr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑌 ) = 𝑌 )
33 24 30 32 3eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) = 𝑌 )
34 33 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) = 𝑌 )
35 34 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑍 ) + ( 𝑍 + 𝑌 ) ) = 𝑌 )
36 4 22 35 3eqtr3d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ) → 𝑋 = 𝑌 )
37 36 exp53 ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 → ( 𝑍 ∈ 𝐵 → ( ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
38 37 3imp2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) → 𝑋 = 𝑌 ) )
39 oveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) )
40 38 39 impbid1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑍 + 𝑋 ) = ( 𝑍 + 𝑌 ) ↔ 𝑋 = 𝑌 ) )