Proof of Theorem mhmlem
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
2 | | mhmlem.a |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | mhmlem.b |
. 2
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
4 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑋 ↔ 𝐴 ∈ 𝑋)) |
5 | 4 | 3anbi2d 1404 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ↔ (𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋))) |
6 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 + 𝑦) = (𝐴 + 𝑦)) |
7 | 6 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝐴 + 𝑦))) |
8 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
9 | 8 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝑦))) |
10 | 7, 9 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ↔ (𝐹‘(𝐴 + 𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝑦)))) |
11 | 5, 10 | imbi12d 334 |
. . . 4
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ↔ ((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝐴 + 𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝑦))))) |
12 | | eleq1 2689 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) |
13 | 12 | 3anbi3d 1405 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ↔ (𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) |
14 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴 + 𝑦) = (𝐴 + 𝐵)) |
15 | 14 | fveq2d 6195 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐹‘(𝐴 + 𝑦)) = (𝐹‘(𝐴 + 𝐵))) |
16 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐹‘𝑦) = (𝐹‘𝐵)) |
17 | 16 | oveq2d 6666 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐹‘𝐴) ⨣ (𝐹‘𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵))) |
18 | 15, 17 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝐹‘(𝐴 + 𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝑦)) ↔ (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))) |
19 | 13, 18 | imbi12d 334 |
. . . 4
⊢ (𝑦 = 𝐵 → (((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝐴 + 𝑦)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝑦))) ↔ ((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵))))) |
20 | | ghmgrp.f |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
21 | 11, 19, 20 | vtocl2g 3270 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))) |
22 | 2, 3, 21 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))) |
23 | 1, 2, 3, 22 | mp3and 1427 |
1
⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵))) |