Proof of Theorem caovdirg
Step | Hyp | Ref
| Expression |
1 | | caovdirg.1 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) |
2 | 1 | ralrimivvva 2553 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝐾 ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) |
3 | | oveq1 5860 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦)) |
4 | 3 | oveq1d 5868 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝐴𝐹𝑦)𝐺𝑧)) |
5 | | oveq1 5860 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥𝐺𝑧) = (𝐴𝐺𝑧)) |
6 | 5 | oveq1d 5868 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)) = ((𝐴𝐺𝑧)𝐻(𝑦𝐺𝑧))) |
7 | 4, 6 | eqeq12d 2185 |
. . 3
⊢ (𝑥 = 𝐴 → (((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)) ↔ ((𝐴𝐹𝑦)𝐺𝑧) = ((𝐴𝐺𝑧)𝐻(𝑦𝐺𝑧)))) |
8 | | oveq2 5861 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵)) |
9 | 8 | oveq1d 5868 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦)𝐺𝑧) = ((𝐴𝐹𝐵)𝐺𝑧)) |
10 | | oveq1 5860 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦𝐺𝑧) = (𝐵𝐺𝑧)) |
11 | 10 | oveq2d 5869 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴𝐺𝑧)𝐻(𝑦𝐺𝑧)) = ((𝐴𝐺𝑧)𝐻(𝐵𝐺𝑧))) |
12 | 9, 11 | eqeq12d 2185 |
. . 3
⊢ (𝑦 = 𝐵 → (((𝐴𝐹𝑦)𝐺𝑧) = ((𝐴𝐺𝑧)𝐻(𝑦𝐺𝑧)) ↔ ((𝐴𝐹𝐵)𝐺𝑧) = ((𝐴𝐺𝑧)𝐻(𝐵𝐺𝑧)))) |
13 | | oveq2 5861 |
. . . 4
⊢ (𝑧 = 𝐶 → ((𝐴𝐹𝐵)𝐺𝑧) = ((𝐴𝐹𝐵)𝐺𝐶)) |
14 | | oveq2 5861 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝐴𝐺𝑧) = (𝐴𝐺𝐶)) |
15 | | oveq2 5861 |
. . . . 5
⊢ (𝑧 = 𝐶 → (𝐵𝐺𝑧) = (𝐵𝐺𝐶)) |
16 | 14, 15 | oveq12d 5871 |
. . . 4
⊢ (𝑧 = 𝐶 → ((𝐴𝐺𝑧)𝐻(𝐵𝐺𝑧)) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |
17 | 13, 16 | eqeq12d 2185 |
. . 3
⊢ (𝑧 = 𝐶 → (((𝐴𝐹𝐵)𝐺𝑧) = ((𝐴𝐺𝑧)𝐻(𝐵𝐺𝑧)) ↔ ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))) |
18 | 7, 12, 17 | rspc3v 2850 |
. 2
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝐾 ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))) |
19 | 2, 18 | mpan9 279 |
1
⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |