| Step | Hyp | Ref
| Expression |
| 1 | | funcco.f |
. . . 4
⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) |
| 2 | | funcco.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐷) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 4 | | funcco.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐷) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(Id‘𝐷) =
(Id‘𝐷) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(Id‘𝐸) =
(Id‘𝐸) |
| 8 | | funcco.o |
. . . . 5
⊢ · =
(comp‘𝐷) |
| 9 | | funcco.O |
. . . . 5
⊢ 𝑂 = (comp‘𝐸) |
| 10 | | df-br 5144 |
. . . . . . . 8
⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸)) |
| 11 | 1, 10 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸)) |
| 12 | | funcrcl 17908 |
. . . . . . 7
⊢
(〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 14 | 13 | simpld 494 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 15 | 13 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) |
| 16 | 2, 3, 4, 5, 6, 7, 8, 9, 14, 15 | isfunc 17909 |
. . . 4
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
| 17 | 1, 16 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
| 18 | 17 | simp3d 1145 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
| 19 | | funcco.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 20 | | funcco.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐵) |
| 22 | | funcco.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 23 | 22 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍 ∈ 𝐵) |
| 24 | | funcco.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (𝑋𝐻𝑌)) |
| 25 | 24 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑀 ∈ (𝑋𝐻𝑌)) |
| 26 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋) |
| 27 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌) |
| 28 | 26, 27 | oveq12d 7449 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
| 29 | 25, 28 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑀 ∈ (𝑥𝐻𝑦)) |
| 30 | | funcco.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (𝑌𝐻𝑍)) |
| 31 | 30 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑁 ∈ (𝑌𝐻𝑍)) |
| 32 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑦 = 𝑌) |
| 33 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑧 = 𝑍) |
| 34 | 32, 33 | oveq12d 7449 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍)) |
| 35 | 31, 34 | eleqtrrd 2844 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → 𝑁 ∈ (𝑦𝐻𝑧)) |
| 36 | | simp-5r 786 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑥 = 𝑋) |
| 37 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑧 = 𝑍) |
| 38 | 36, 37 | oveq12d 7449 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑥𝐺𝑧) = (𝑋𝐺𝑍)) |
| 39 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑦 = 𝑌) |
| 40 | 36, 39 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑌〉) |
| 41 | 40, 37 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑋, 𝑌〉 · 𝑍)) |
| 42 | | simpr 484 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
| 43 | | simplr 769 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 𝑚 = 𝑀) |
| 44 | 41, 42, 43 | oveq123d 7452 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚) = (𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) |
| 45 | 38, 44 | fveq12d 6913 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀))) |
| 46 | 36 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹‘𝑥) = (𝐹‘𝑋)) |
| 47 | 39 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹‘𝑦) = (𝐹‘𝑌)) |
| 48 | 46, 47 | opeq12d 4881 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘𝑋), (𝐹‘𝑌)〉) |
| 49 | 37 | fveq2d 6910 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝐹‘𝑧) = (𝐹‘𝑍)) |
| 50 | 48, 49 | oveq12d 7449 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧)) = (〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))) |
| 51 | 39, 37 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑦𝐺𝑧) = (𝑌𝐺𝑍)) |
| 52 | 51, 42 | fveq12d 6913 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑦𝐺𝑧)‘𝑛) = ((𝑌𝐺𝑍)‘𝑁)) |
| 53 | 36, 39 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (𝑥𝐺𝑦) = (𝑋𝐺𝑌)) |
| 54 | 53, 43 | fveq12d 6913 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → ((𝑥𝐺𝑦)‘𝑚) = ((𝑋𝐺𝑌)‘𝑀)) |
| 55 | 50, 52, 54 | oveq123d 7452 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀))) |
| 56 | 45, 55 | eqeq12d 2753 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) ∧ 𝑛 = 𝑁) → (((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) ↔ ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 57 | 35, 56 | rspcdv 3614 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑚 = 𝑀) → (∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 58 | 29, 57 | rspcimdv 3612 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 59 | 23, 58 | rspcimdv 3612 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 60 | 21, 59 | rspcimdv 3612 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 61 | 60 | adantld 490 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 62 | 19, 61 | rspcimdv 3612 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀)))) |
| 63 | 18, 62 | mpd 15 |
1
⊢ (𝜑 → ((𝑋𝐺𝑍)‘(𝑁(〈𝑋, 𝑌〉 · 𝑍)𝑀)) = (((𝑌𝐺𝑍)‘𝑁)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉𝑂(𝐹‘𝑍))((𝑋𝐺𝑌)‘𝑀))) |