Metamath Proof Explorer

Theorem grprcan

Description: Right cancellation law for groups. (Contributed by NM, 24-Aug-2011) (Proof shortened by Mario Carneiro, 6-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 grprcan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grprcan.p ⊢ + = ( +g ‘ 𝐺 )
3 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
4 1 2 3 grpinvex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) )
5 4 3ad2antr3 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) )
6 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) )
7 6 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( ( 𝑋 + 𝑍 ) + 𝑦 ) = ( ( 𝑌 + 𝑍 ) + 𝑦 ) )
8 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝐺 ∈ Grp )
9 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
10 8 9 sylan ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 + 𝑣 ) + 𝑤 ) = ( 𝑢 + ( 𝑣 + 𝑤 ) ) )
11 simplr1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑋 ∈ 𝐵 )
12 simplr3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑍 ∈ 𝐵 )
13 simprll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑦 ∈ 𝐵 )
14 10 11 12 13 caovassd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( ( 𝑋 + 𝑍 ) + 𝑦 ) = ( 𝑋 + ( 𝑍 + 𝑦 ) ) )
15 simplr2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑌 ∈ 𝐵 )
16 10 15 12 13 caovassd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( ( 𝑌 + 𝑍 ) + 𝑦 ) = ( 𝑌 + ( 𝑍 + 𝑦 ) ) )
17 7 14 16 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + ( 𝑍 + 𝑦 ) ) = ( 𝑌 + ( 𝑍 + 𝑦 ) ) )
18 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
19 8 18 syl3an1 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
20 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
21 8 20 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
22 1 2 3 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
23 8 22 sylan ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
24 1 2 3 grpinvex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ) → ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑢 ) = ( 0g ‘ 𝐺 ) )
25 8 24 sylan ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑢 ∈ 𝐵 ) → ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑢 ) = ( 0g ‘ 𝐺 ) )
26 simpr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
27 13 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑍 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
28 simprlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) )
29 28 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) )
30 19 21 23 10 25 26 27 29 grprinvd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 + 𝑦 ) = ( 0g ‘ 𝐺 ) )
31 12 30 mpdan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑍 + 𝑦 ) = ( 0g ‘ 𝐺 ) )
32 31 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + ( 𝑍 + 𝑦 ) ) = ( 𝑋 + ( 0g ‘ 𝐺 ) ) )
33 31 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑌 + ( 𝑍 + 𝑦 ) ) = ( 𝑌 + ( 0g ‘ 𝐺 ) ) )
34 17 32 33 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = ( 𝑌 + ( 0g ‘ 𝐺 ) ) )
35 1 2 3 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
36 8 11 35 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
37 1 2 3 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 + ( 0g ‘ 𝐺 ) ) = 𝑌 )
38 8 15 37 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑌 + ( 0g ‘ 𝐺 ) ) = 𝑌 )
39 34 36 38 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑋 = 𝑌 )
40 39 expr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) )
41 5 40 rexlimddv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) )
42 oveq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) )
43 41 42 impbid1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ↔ 𝑋 = 𝑌 ) )