Step | Hyp | Ref
| Expression |
1 | | estrcbas.c |
. . . 4
⊢ 𝐶 = (ExtStrCat‘𝑈) |
2 | | estrcbas.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
3 | | estrcco.o |
. . . 4
⊢ · =
(comp‘𝐶) |
4 | 1, 2, 3 | estrccofval 16592 |
. . 3
⊢ (𝜑 → · = (𝑣 ∈ (𝑈 × 𝑈), 𝑧 ∈ 𝑈 ↦ (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (Base‘𝑧) = (Base‘𝑍)) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍) → (Base‘𝑧) = (Base‘𝑍)) |
7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘𝑧) = (Base‘𝑍)) |
8 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑣 = 〈𝑋, 𝑌〉) |
9 | 8 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑣) = (2nd
‘〈𝑋, 𝑌〉)) |
10 | | estrcco.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
11 | | estrcco.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
12 | | op2ndg 7072 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
15 | 9, 14 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑣) = 𝑌) |
16 | 15 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(2nd
‘𝑣)) =
(Base‘𝑌)) |
17 | 7, 16 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))) = ((Base‘𝑍) ↑𝑚
(Base‘𝑌))) |
18 | 8 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑣) = (1st
‘〈𝑋, 𝑌〉)) |
19 | 18 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘𝑣)) =
(Base‘(1st ‘〈𝑋, 𝑌〉))) |
20 | | op1stg 7071 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
21 | 10, 11, 20 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
22 | 21 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(1st ‘〈𝑋, 𝑌〉)) = (Base‘𝑋)) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘〈𝑋, 𝑌〉)) = (Base‘𝑋)) |
24 | 19, 23 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (Base‘(1st
‘𝑣)) =
(Base‘𝑋)) |
25 | 16, 24 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) = ((Base‘𝑌) ↑𝑚
(Base‘𝑋))) |
26 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (𝑔 ∘ 𝑓) = (𝑔 ∘ 𝑓)) |
27 | 17, 25, 26 | mpt2eq123dv 6615 |
. . 3
⊢ ((𝜑 ∧ (𝑣 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (𝑔 ∈ ((Base‘𝑧) ↑𝑚
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑𝑚 (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)) = (𝑔 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↦
(𝑔 ∘ 𝑓))) |
28 | | opelxpi 5072 |
. . . 4
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑈)) |
29 | 10, 11, 28 | syl2anc 691 |
. . 3
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝑈 × 𝑈)) |
30 | | estrcco.z |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
31 | | ovex 6577 |
. . . . 5
⊢
((Base‘𝑍)
↑𝑚 (Base‘𝑌)) ∈ V |
32 | | ovex 6577 |
. . . . 5
⊢
((Base‘𝑌)
↑𝑚 (Base‘𝑋)) ∈ V |
33 | 31, 32 | mpt2ex 7136 |
. . . 4
⊢ (𝑔 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↦
(𝑔 ∘ 𝑓)) ∈ V |
34 | 33 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑔 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↦
(𝑔 ∘ 𝑓)) ∈ V) |
35 | 4, 27, 29, 30, 34 | ovmpt2d 6686 |
. 2
⊢ (𝜑 → (〈𝑋, 𝑌〉 · 𝑍) = (𝑔 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)), 𝑓 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↦
(𝑔 ∘ 𝑓))) |
36 | | simpl 472 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → 𝑔 = 𝐺) |
37 | | simpr 476 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
38 | 36, 37 | coeq12d 5208 |
. . 3
⊢ ((𝑔 = 𝐺 ∧ 𝑓 = 𝐹) → (𝑔 ∘ 𝑓) = (𝐺 ∘ 𝐹)) |
39 | 38 | adantl 481 |
. 2
⊢ ((𝜑 ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (𝑔 ∘ 𝑓) = (𝐺 ∘ 𝐹)) |
40 | | estrcco.g |
. . . 4
⊢ (𝜑 → 𝐺:𝐵⟶𝐷) |
41 | | estrcco.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
42 | 41 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑌)) |
43 | 42 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (Base‘𝑌) = 𝐵) |
44 | | estrcco.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝑍) |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (Base‘𝑍)) |
46 | 45 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (Base‘𝑍) = 𝐷) |
47 | 43, 46 | feq23d 5953 |
. . . 4
⊢ (𝜑 → (𝐺:(Base‘𝑌)⟶(Base‘𝑍) ↔ 𝐺:𝐵⟶𝐷)) |
48 | 40, 47 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐺:(Base‘𝑌)⟶(Base‘𝑍)) |
49 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑍)
∈ V |
50 | 49 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑍) ∈ V) |
51 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑌)
∈ V |
52 | 51 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
53 | | elmapg 7757 |
. . . 4
⊢
(((Base‘𝑍)
∈ V ∧ (Base‘𝑌) ∈ V) → (𝐺 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)) ↔
𝐺:(Base‘𝑌)⟶(Base‘𝑍))) |
54 | 50, 52, 53 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐺 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)) ↔
𝐺:(Base‘𝑌)⟶(Base‘𝑍))) |
55 | 48, 54 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐺 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌))) |
56 | | estrcco.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
57 | | estrcco.a |
. . . . . . 7
⊢ 𝐴 = (Base‘𝑋) |
58 | 57 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐴 = (Base‘𝑋)) |
59 | 58 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (Base‘𝑋) = 𝐴) |
60 | 59, 43 | feq23d 5953 |
. . . 4
⊢ (𝜑 → (𝐹:(Base‘𝑋)⟶(Base‘𝑌) ↔ 𝐹:𝐴⟶𝐵)) |
61 | 56, 60 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐹:(Base‘𝑋)⟶(Base‘𝑌)) |
62 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑋)
∈ V |
63 | 62 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑋) ∈ V) |
64 | | elmapg 7757 |
. . . 4
⊢
(((Base‘𝑌)
∈ V ∧ (Base‘𝑋) ∈ V) → (𝐹 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↔
𝐹:(Base‘𝑋)⟶(Base‘𝑌))) |
65 | 52, 63, 64 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐹 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋)) ↔
𝐹:(Base‘𝑋)⟶(Base‘𝑌))) |
66 | 61, 65 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐹 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋))) |
67 | | coexg 7010 |
. . 3
⊢ ((𝐺 ∈ ((Base‘𝑍) ↑𝑚
(Base‘𝑌)) ∧ 𝐹 ∈ ((Base‘𝑌) ↑𝑚
(Base‘𝑋))) →
(𝐺 ∘ 𝐹) ∈ V) |
68 | 55, 66, 67 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ V) |
69 | 35, 39, 55, 66, 68 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺 ∘ 𝐹)) |