Proof of Theorem grpsubadd
| Step | Hyp | Ref
| Expression |
| 1 | | grpsubadd.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | grpsubadd.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
| 3 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 4 | | grpsubadd.m |
. . . . . . 7
⊢ − =
(-g‘𝐺) |
| 5 | 1, 2, 3, 4 | grpsubval 19003 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 +
((invg‘𝐺)‘𝑌))) |
| 6 | 5 | 3adant3 1133 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 +
((invg‘𝐺)‘𝑌))) |
| 7 | 6 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − 𝑌) = (𝑋 +
((invg‘𝐺)‘𝑌))) |
| 8 | 7 | eqeq1d 2739 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑋 +
((invg‘𝐺)‘𝑌)) = 𝑍)) |
| 9 | | simpl 482 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐺 ∈ Grp) |
| 10 | | simpr1 1195 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 11 | 1, 3 | grpinvcl 19005 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((invg‘𝐺)‘𝑌) ∈ 𝐵) |
| 12 | 11 | 3ad2antr2 1190 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((invg‘𝐺)‘𝑌) ∈ 𝐵) |
| 13 | 1, 2 | grpcl 18959 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑌) ∈ 𝐵) → (𝑋 +
((invg‘𝐺)‘𝑌)) ∈ 𝐵) |
| 14 | 9, 10, 12, 13 | syl3anc 1373 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 +
((invg‘𝐺)‘𝑌)) ∈ 𝐵) |
| 15 | | simpr3 1197 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) |
| 16 | | simpr2 1196 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
| 17 | 1, 2 | grprcan 18991 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ ((𝑋 +
((invg‘𝐺)‘𝑌)) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = (𝑍 + 𝑌) ↔ (𝑋 +
((invg‘𝐺)‘𝑌)) = 𝑍)) |
| 18 | 9, 14, 15, 16, 17 | syl13anc 1374 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = (𝑍 + 𝑌) ↔ (𝑋 +
((invg‘𝐺)‘𝑌)) = 𝑍)) |
| 19 | 1, 2 | grpass 18960 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = (𝑋 +
(((invg‘𝐺)‘𝑌) + 𝑌))) |
| 20 | 9, 10, 12, 16, 19 | syl13anc 1374 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = (𝑋 +
(((invg‘𝐺)‘𝑌) + 𝑌))) |
| 21 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 22 | 1, 2, 21, 3 | grplinv 19007 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → (((invg‘𝐺)‘𝑌) + 𝑌) = (0g‘𝐺)) |
| 23 | 22 | 3ad2antr2 1190 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((invg‘𝐺)‘𝑌) + 𝑌) = (0g‘𝐺)) |
| 24 | 23 | oveq2d 7447 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 +
(((invg‘𝐺)‘𝑌) + 𝑌)) = (𝑋 + (0g‘𝐺))) |
| 25 | 1, 2, 21 | grprid 18986 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (0g‘𝐺)) = 𝑋) |
| 26 | 25 | 3ad2antr1 1189 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 + (0g‘𝐺)) = 𝑋) |
| 27 | 20, 24, 26 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = 𝑋) |
| 28 | 27 | eqeq1d 2739 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 +
((invg‘𝐺)‘𝑌)) + 𝑌) = (𝑍 + 𝑌) ↔ 𝑋 = (𝑍 + 𝑌))) |
| 29 | 8, 18, 28 | 3bitr2d 307 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ 𝑋 = (𝑍 + 𝑌))) |
| 30 | | eqcom 2744 |
. 2
⊢ (𝑋 = (𝑍 + 𝑌) ↔ (𝑍 + 𝑌) = 𝑋) |
| 31 | 29, 30 | bitrdi 287 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋)) |