| Step | Hyp | Ref
| Expression |
| 1 | | estrcbas.c |
. . . 4
⊢ 𝐶 = (ExtStrCat‘𝑈) |
| 2 | | estrcbas.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
| 3 | | estrcco.o |
. . . 4
⊢ · =
(comp‘𝐶) |
| 4 | 1, 2, 3 | estrccofval 18173 |
. . 3
⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (Base‘𝑧) = (Base‘𝑍)) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍) → (Base‘𝑧) = (Base‘𝑍)) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘𝑧) = (Base‘𝑍)) |
| 8 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑣 = 〈𝑋, 𝑌〉) |
| 9 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑣) = (2nd
‘〈𝑋, 𝑌〉)) |
| 10 | | estrcco.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
| 11 | | estrcco.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
| 12 | | op2ndg 8027 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
| 13 | 10, 11, 12 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
| 15 | 9, 14 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑣) = 𝑌) |
| 16 | 15 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(2nd
‘𝑣)) =
(Base‘𝑌)) |
| 17 | 7, 16 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))) = ((Base‘𝑍) ↑m (Base‘𝑌))) |
| 18 | 8 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑣) = (1st
‘〈𝑋, 𝑌〉)) |
| 19 | 18 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘𝑣)) =
(Base‘(1st ‘〈𝑋, 𝑌〉))) |
| 20 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
| 21 | 10, 11, 20 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
| 22 | 21 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(1st ‘〈𝑋, 𝑌〉)) = (Base‘𝑋)) |
| 23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘〈𝑋, 𝑌〉)) = (Base‘𝑋)) |
| 24 | 19, 23 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘𝑣)) =
(Base‘𝑋)) |
| 25 | 16, 24 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) = ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 26 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (𝑔 ∘ 𝑓) = (𝑔 ∘ 𝑓)) |
| 27 | 17, 25, 26 | mpoeq123dv 7508 |
. . 3
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((Base‘𝑍) ↑m (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) ↦ (𝑔 ∘ 𝑓))) |
| 28 | 10, 11 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑈)) |
| 29 | | estrcco.z |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 30 | | ovex 7464 |
. . . . 5
⊢
((Base‘𝑍)
↑m (Base‘𝑌)) ∈ V |
| 31 | | ovex 7464 |
. . . . 5
⊢
((Base‘𝑌)
↑m (Base‘𝑋)) ∈ V |
| 32 | 30, 31 | mpoex 8104 |
. . . 4
⊢ (𝑔 ∈ ((Base‘𝑍) ↑m
(Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑m
(Base‘𝑋)) ↦
(𝑔 ∘ 𝑓)) ∈ V |
| 33 | 32 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑔 ∈ ((Base‘𝑍) ↑m (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) ↦ (𝑔 ∘ 𝑓)) ∈ V) |
| 34 | 4, 27, 28, 29, 33 | ovmpod 7585 |
. 2
⊢ (𝜑 → (〈𝑋, 𝑌〉 · 𝑍) = (𝑔 ∈ ((Base‘𝑍) ↑m (Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) ↦ (𝑔 ∘ 𝑓))) |
| 35 | | simpl 482 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → 𝑔 = 𝐺) |
| 36 | | simpr 484 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
| 37 | 35, 36 | coeq12d 5875 |
. . 3
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → (𝑔 ∘ 𝑓) = (𝐺 ∘ 𝐹)) |
| 38 | 37 | adantl 481 |
. 2
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (𝑔 ∘ 𝑓) = (𝐺 ∘ 𝐹)) |
| 39 | | estrcco.g |
. . . 4
⊢ (𝜑 → 𝐺:𝐵⟶𝐷) |
| 40 | | estrcco.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
| 41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑌)) |
| 42 | 41 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (Base‘𝑌) = 𝐵) |
| 43 | | estrcco.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝑍) |
| 44 | 43 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (Base‘𝑍)) |
| 45 | 44 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (Base‘𝑍) = 𝐷) |
| 46 | 42, 45 | feq23d 6731 |
. . . 4
⊢ (𝜑 → (𝐺:(Base‘𝑌)⟶(Base‘𝑍) ↔ 𝐺:𝐵⟶𝐷)) |
| 47 | 39, 46 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍)) |
| 48 | | fvexd 6921 |
. . . 4
⊢ (𝜑 → (Base‘𝑍) ∈ V) |
| 49 | | fvexd 6921 |
. . . 4
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
| 50 | 48, 49 | elmapd 8880 |
. . 3
⊢ (𝜑 → (𝐺 ∈ ((Base‘𝑍) ↑m (Base‘𝑌)) ↔ 𝐺:(Base‘𝑌)⟶(Base‘𝑍))) |
| 51 | 47, 50 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐺 ∈ ((Base‘𝑍) ↑m (Base‘𝑌))) |
| 52 | | estrcco.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 53 | | estrcco.a |
. . . . . . 7
⊢ 𝐴 = (Base‘𝑋) |
| 54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐴 = (Base‘𝑋)) |
| 55 | 54 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (Base‘𝑋) = 𝐴) |
| 56 | 55, 42 | feq23d 6731 |
. . . 4
⊢ (𝜑 → (𝐹:(Base‘𝑋)⟶(Base‘𝑌) ↔ 𝐹:𝐴⟶𝐵)) |
| 57 | 52, 56 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
| 58 | | fvexd 6921 |
. . . 4
⊢ (𝜑 → (Base‘𝑋) ∈ V) |
| 59 | 49, 58 | elmapd 8880 |
. . 3
⊢ (𝜑 → (𝐹 ∈ ((Base‘𝑌) ↑m (Base‘𝑋)) ↔ 𝐹:(Base‘𝑋)⟶(Base‘𝑌))) |
| 60 | 57, 59 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐹 ∈ ((Base‘𝑌) ↑m (Base‘𝑋))) |
| 61 | | coexg 7951 |
. . 3
⊢ ((𝐺 ∈ ((Base‘𝑍) ↑m
(Base‘𝑌)) ∧ 𝐹 ∈ ((Base‘𝑌) ↑m
(Base‘𝑋))) →
(𝐺 ∘ 𝐹) ∈ V) |
| 62 | 51, 60, 61 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ V) |
| 63 | 34, 38, 51, 60, 62 | ovmpod 7585 |
1
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) |