Step | Hyp | Ref
| Expression |
1 | | grprinvlem.n |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂) |
2 | 1 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂) |
3 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑦 + 𝑥) = (𝑦 + 𝑧)) |
4 | 3 | eqeq1d 2179 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑦 + 𝑥) = 𝑂 ↔ (𝑦 + 𝑧) = 𝑂)) |
5 | 4 | rexbidv 2471 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂 ↔ ∃𝑦 ∈ 𝐵 (𝑦 + 𝑧) = 𝑂)) |
6 | 5 | cbvralvw 2700 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂 ↔ ∀𝑧 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑦 + 𝑧) = 𝑂) |
7 | 2, 6 | sylib 121 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑦 + 𝑧) = 𝑂) |
8 | | grprinvlem.x |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵) |
9 | | oveq2 5861 |
. . . . . 6
⊢ (𝑧 = 𝑋 → (𝑦 + 𝑧) = (𝑦 + 𝑋)) |
10 | 9 | eqeq1d 2179 |
. . . . 5
⊢ (𝑧 = 𝑋 → ((𝑦 + 𝑧) = 𝑂 ↔ (𝑦 + 𝑋) = 𝑂)) |
11 | 10 | rexbidv 2471 |
. . . 4
⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐵 (𝑦 + 𝑧) = 𝑂 ↔ ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 𝑂)) |
12 | 11 | rspccva 2833 |
. . 3
⊢
((∀𝑧 ∈
𝐵 ∃𝑦 ∈ 𝐵 (𝑦 + 𝑧) = 𝑂 ∧ 𝑋 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 𝑂) |
13 | 7, 8, 12 | syl2an2r 590 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 𝑂) |
14 | | grprinvlem.e |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑋) = 𝑋) |
15 | 14 | oveq2d 5869 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑦 + (𝑋 + 𝑋)) = (𝑦 + 𝑋)) |
16 | 15 | adantr 274 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → (𝑦 + (𝑋 + 𝑋)) = (𝑦 + 𝑋)) |
17 | | simprr 527 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → (𝑦 + 𝑋) = 𝑂) |
18 | 17 | oveq1d 5868 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → ((𝑦 + 𝑋) + 𝑋) = (𝑂 + 𝑋)) |
19 | | grprinvlem.a |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
20 | 19 | caovassg 6011 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
21 | 20 | ad4ant14 511 |
. . . . 5
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
22 | | simprl 526 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → 𝑦 ∈ 𝐵) |
23 | 8 | adantr 274 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → 𝑋 ∈ 𝐵) |
24 | 21, 22, 23, 23 | caovassd 6012 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → ((𝑦 + 𝑋) + 𝑋) = (𝑦 + (𝑋 + 𝑋))) |
25 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (𝑂 + 𝑦) = (𝑂 + 𝑋)) |
26 | | id 19 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → 𝑦 = 𝑋) |
27 | 25, 26 | eqeq12d 2185 |
. . . . . 6
⊢ (𝑦 = 𝑋 → ((𝑂 + 𝑦) = 𝑦 ↔ (𝑂 + 𝑋) = 𝑋)) |
28 | | grprinvlem.i |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥) |
29 | 28 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑂 + 𝑥) = 𝑥) |
30 | | oveq2 5861 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑂 + 𝑥) = (𝑂 + 𝑦)) |
31 | | id 19 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
32 | 30, 31 | eqeq12d 2185 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑂 + 𝑥) = 𝑥 ↔ (𝑂 + 𝑦) = 𝑦)) |
33 | 32 | cbvralvw 2700 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 (𝑂 + 𝑥) = 𝑥 ↔ ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
34 | 29, 33 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
35 | 34 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ∀𝑦 ∈ 𝐵 (𝑂 + 𝑦) = 𝑦) |
36 | 27, 35, 8 | rspcdva 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑂 + 𝑋) = 𝑋) |
37 | 36 | adantr 274 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → (𝑂 + 𝑋) = 𝑋) |
38 | 18, 24, 37 | 3eqtr3d 2211 |
. . 3
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → (𝑦 + (𝑋 + 𝑋)) = 𝑋) |
39 | 16, 38, 17 | 3eqtr3d 2211 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 + 𝑋) = 𝑂)) → 𝑋 = 𝑂) |
40 | 13, 39 | rexlimddv 2592 |
1
⊢ ((𝜑 ∧ 𝜓) → 𝑋 = 𝑂) |