Proof of Theorem grpsubsub4
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐺 ∈ Grp) |
| 2 | | grpsubadd.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
| 3 | | grpsubadd.m |
. . . . . . . 8
⊢ − =
(-g‘𝐺) |
| 4 | 2, 3 | grpsubcl 19038 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) |
| 5 | 4 | 3adant3r3 1185 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − 𝑌) ∈ 𝐵) |
| 6 | | simpr3 1197 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) |
| 7 | | grpsubadd.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
| 8 | 2, 7, 3 | grpnpcan 19050 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 − 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 − 𝑌) − 𝑍) + 𝑍) = (𝑋 − 𝑌)) |
| 9 | 1, 5, 6, 8 | syl3anc 1373 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) − 𝑍) + 𝑍) = (𝑋 − 𝑌)) |
| 10 | 9 | oveq1d 7446 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((𝑋 − 𝑌) − 𝑍) + 𝑍) + 𝑌) = ((𝑋 − 𝑌) + 𝑌)) |
| 11 | 2, 3 | grpsubcl 19038 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑋 − 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 − 𝑌) − 𝑍) ∈ 𝐵) |
| 12 | 1, 5, 6, 11 | syl3anc 1373 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) ∈ 𝐵) |
| 13 | | simpr2 1196 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) |
| 14 | 2, 7 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (((𝑋 − 𝑌) − 𝑍) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((((𝑋 − 𝑌) − 𝑍) + 𝑍) + 𝑌) = (((𝑋 − 𝑌) − 𝑍) + (𝑍 + 𝑌))) |
| 15 | 1, 12, 6, 13, 14 | syl13anc 1374 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((𝑋 − 𝑌) − 𝑍) + 𝑍) + 𝑌) = (((𝑋 − 𝑌) − 𝑍) + (𝑍 + 𝑌))) |
| 16 | 2, 7, 3 | grpnpcan 19050 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋) |
| 17 | 16 | 3adant3r3 1185 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑌) = 𝑋) |
| 18 | 10, 15, 17 | 3eqtr3d 2785 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) − 𝑍) + (𝑍 + 𝑌)) = 𝑋) |
| 19 | | simpr1 1195 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 20 | 2, 7 | grpcl 18959 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑍 + 𝑌) ∈ 𝐵) |
| 21 | 1, 6, 13, 20 | syl3anc 1373 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 + 𝑌) ∈ 𝐵) |
| 22 | 2, 7, 3 | grpsubadd 19046 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ (𝑍 + 𝑌) ∈ 𝐵 ∧ ((𝑋 − 𝑌) − 𝑍) ∈ 𝐵)) → ((𝑋 − (𝑍 + 𝑌)) = ((𝑋 − 𝑌) − 𝑍) ↔ (((𝑋 − 𝑌) − 𝑍) + (𝑍 + 𝑌)) = 𝑋)) |
| 23 | 1, 19, 21, 12, 22 | syl13anc 1374 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − (𝑍 + 𝑌)) = ((𝑋 − 𝑌) − 𝑍) ↔ (((𝑋 − 𝑌) − 𝑍) + (𝑍 + 𝑌)) = 𝑋)) |
| 24 | 18, 23 | mpbird 257 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑍 + 𝑌)) = ((𝑋 − 𝑌) − 𝑍)) |
| 25 | 24 | eqcomd 2743 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌))) |