| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | natixp.2 | . . . 4
⊢ (𝜑 → 𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉)) | 
| 2 |  | natrcl.1 | . . . . 5
⊢ 𝑁 = (𝐶 Nat 𝐷) | 
| 3 |  | natixp.b | . . . . 5
⊢ 𝐵 = (Base‘𝐶) | 
| 4 |  | nati.h | . . . . 5
⊢ 𝐻 = (Hom ‘𝐶) | 
| 5 |  | eqid 2736 | . . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 6 |  | nati.o | . . . . 5
⊢  · =
(comp‘𝐷) | 
| 7 | 2 | natrcl 17999 | . . . . . . . 8
⊢ (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) → (〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) ∧ 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷))) | 
| 8 | 1, 7 | syl 17 | . . . . . . 7
⊢ (𝜑 → (〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) ∧ 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷))) | 
| 9 | 8 | simpld 494 | . . . . . 6
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) | 
| 10 |  | df-br 5143 | . . . . . 6
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) | 
| 11 | 9, 10 | sylibr 234 | . . . . 5
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | 
| 12 | 8 | simprd 495 | . . . . . 6
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷)) | 
| 13 |  | df-br 5143 | . . . . . 6
⊢ (𝐾(𝐶 Func 𝐷)𝐿 ↔ 〈𝐾, 𝐿〉 ∈ (𝐶 Func 𝐷)) | 
| 14 | 12, 13 | sylibr 234 | . . . . 5
⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | 
| 15 | 2, 3, 4, 5, 6, 11,
14 | isnat 17996 | . . . 4
⊢ (𝜑 → (𝐴 ∈ (〈𝐹, 𝐺〉𝑁〈𝐾, 𝐿〉) ↔ (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)(Hom ‘𝐷)(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))))) | 
| 16 | 1, 15 | mpbid 232 | . . 3
⊢ (𝜑 → (𝐴 ∈ X𝑥 ∈ 𝐵 ((𝐹‘𝑥)(Hom ‘𝐷)(𝐾‘𝑥)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)))) | 
| 17 | 16 | simprd 495 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥))) | 
| 18 |  | nati.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 19 |  | nati.y | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 20 | 19 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐵) | 
| 21 |  | nati.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝑋𝐻𝑌)) | 
| 22 | 21 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑅 ∈ (𝑋𝐻𝑌)) | 
| 23 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑥 = 𝑋) | 
| 24 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) | 
| 25 | 23, 24 | oveq12d 7450 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) | 
| 26 | 22, 25 | eleqtrrd 2843 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑅 ∈ (𝑥𝐻𝑦)) | 
| 27 |  | simpllr 775 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑥 = 𝑋) | 
| 28 | 27 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐹‘𝑥) = (𝐹‘𝑋)) | 
| 29 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑦 = 𝑌) | 
| 30 | 29 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐹‘𝑦) = (𝐹‘𝑌)) | 
| 31 | 28, 30 | opeq12d 4880 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘𝑋), (𝐹‘𝑌)〉) | 
| 32 | 29 | fveq2d 6909 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐾‘𝑦) = (𝐾‘𝑌)) | 
| 33 | 31, 32 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦)) = (〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))) | 
| 34 | 29 | fveq2d 6909 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐴‘𝑦) = (𝐴‘𝑌)) | 
| 35 | 27, 29 | oveq12d 7450 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝑥𝐺𝑦) = (𝑋𝐺𝑌)) | 
| 36 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑓 = 𝑅) | 
| 37 | 35, 36 | fveq12d 6912 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝑥𝐺𝑦)‘𝑓) = ((𝑋𝐺𝑌)‘𝑅)) | 
| 38 | 33, 34, 37 | oveq123d 7453 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅))) | 
| 39 | 27 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐾‘𝑥) = (𝐾‘𝑋)) | 
| 40 | 28, 39 | opeq12d 4880 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 〈(𝐹‘𝑥), (𝐾‘𝑥)〉 = 〈(𝐹‘𝑋), (𝐾‘𝑋)〉) | 
| 41 | 40, 32 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦)) = (〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))) | 
| 42 | 27, 29 | oveq12d 7450 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝑥𝐿𝑦) = (𝑋𝐿𝑌)) | 
| 43 | 42, 36 | fveq12d 6912 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝑥𝐿𝑦)‘𝑓) = ((𝑋𝐿𝑌)‘𝑅)) | 
| 44 | 27 | fveq2d 6909 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐴‘𝑥) = (𝐴‘𝑋)) | 
| 45 | 41, 43, 44 | oveq123d 7453 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋))) | 
| 46 | 38, 45 | eqeq12d 2752 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)) ↔ ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋)))) | 
| 47 | 26, 46 | rspcdv 3613 | . . . 4
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)) → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋)))) | 
| 48 | 20, 47 | rspcimdv 3611 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)) → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋)))) | 
| 49 | 18, 48 | rspcimdv 3611 | . 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴‘𝑦)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 · (𝐾‘𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(〈(𝐹‘𝑥), (𝐾‘𝑥)〉 · (𝐾‘𝑦))(𝐴‘𝑥)) → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋)))) | 
| 50 | 17, 49 | mpd 15 | 1
⊢ (𝜑 → ((𝐴‘𝑌)(〈(𝐹‘𝑋), (𝐹‘𝑌)〉 · (𝐾‘𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(〈(𝐹‘𝑋), (𝐾‘𝑋)〉 · (𝐾‘𝑌))(𝐴‘𝑋))) |