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
|
grpinva |
⊢ ( ( ( ( 𝐺 ∈ 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 8 11
|
grpridd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 ) |
36 |
1 2 3 8 15
|
grpridd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → ( 𝑌 + ( 0g ‘ 𝐺 ) ) = 𝑌 ) |
37 |
34 35 36
|
3eqtr3d |
⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ∧ ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) ) → 𝑋 = 𝑌 ) |
38 |
37
|
expr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 + 𝑍 ) = ( 0g ‘ 𝐺 ) ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) ) |
39 |
5 38
|
rexlimddv |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) → 𝑋 = 𝑌 ) ) |
40 |
|
oveq1 |
⊢ ( 𝑋 = 𝑌 → ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ) |
41 |
39 40
|
impbid1 |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑌 + 𝑍 ) ↔ 𝑋 = 𝑌 ) ) |