Step | Hyp | Ref
| Expression |
1 | | grprinvlem.c |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
2 | | grprinvlem.o |
. 2
⊢ (𝜑 → 𝑂 ∈ 𝐵) |
3 | | grprinvlem.i |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥) |
4 | | grprinvlem.a |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
5 | | grprinvlem.n |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂) |
6 | 1 | 3expb 1105 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
7 | 6 | caovclg 5653 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢 + 𝑣) ∈ 𝐵) |
8 | 7 | adantlr 446 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢 + 𝑣) ∈ 𝐵) |
9 | | grprinvd.x |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵) |
10 | | grprinvd.n |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝐵) |
11 | 8, 9, 10 | caovcld 5654 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑁) ∈ 𝐵) |
12 | 4 | caovassg 5659 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
13 | 12 | adantlr 446 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
14 | 13, 9, 10, 11 | caovassd 5660 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + (𝑁 + (𝑋 + 𝑁)))) |
15 | | grprinvd.e |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (𝑁 + 𝑋) = 𝑂) |
16 | 15 | oveq1d 5527 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 𝑋) + 𝑁) = (𝑂 + 𝑁)) |
17 | 13, 10, 9, 10 | caovassd 5660 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 𝑋) + 𝑁) = (𝑁 + (𝑋 + 𝑁))) |
18 | 3 | ralrimiva 2392 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑂 + 𝑥) = 𝑥) |
19 | | oveq2 5520 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑂 + 𝑥) = (𝑂 + 𝑦)) |
20 | | id 19 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
21 | 19, 20 | eqeq12d 2054 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑂 + 𝑥) = 𝑥 ↔ (𝑂 + 𝑦) = 𝑦)) |
22 | 21 | cbvralv 2533 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 (𝑂 + 𝑥) = 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
23 | 18, 22 | sylib 127 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
24 | 23 | adantr 261 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
25 | | oveq2 5520 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝑂 + 𝑦) = (𝑂 + 𝑁)) |
26 | | id 19 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → 𝑦 = 𝑁) |
27 | 25, 26 | eqeq12d 2054 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → ((𝑂 + 𝑦) = 𝑦 ↔ (𝑂 + 𝑁) = 𝑁)) |
28 | 27 | rspcv 2652 |
. . . . . 6
⊢ (𝑁 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦 → (𝑂 + 𝑁) = 𝑁)) |
29 | 10, 24, 28 | sylc 56 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑂 + 𝑁) = 𝑁) |
30 | 16, 17, 29 | 3eqtr3d 2080 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑁 + (𝑋 + 𝑁)) = 𝑁) |
31 | 30 | oveq2d 5528 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑋 + (𝑁 + (𝑋 + 𝑁))) = (𝑋 + 𝑁)) |
32 | 14, 31 | eqtrd 2072 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑋 + 𝑁) + (𝑋 + 𝑁)) = (𝑋 + 𝑁)) |
33 | 1, 2, 3, 4, 5, 11,
32 | grprinvlem 5695 |
1
⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑁) = 𝑂) |