Step | Hyp | Ref
| Expression |
1 | | fucco.q |
. . . 4
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
2 | | eqid 2610 |
. . . 4
⊢ (𝐶 Func 𝐷) = (𝐶 Func 𝐷) |
3 | | fucco.n |
. . . 4
⊢ 𝑁 = (𝐶 Nat 𝐷) |
4 | | fucco.a |
. . . 4
⊢ 𝐴 = (Base‘𝐶) |
5 | | fucco.o |
. . . 4
⊢ · =
(comp‘𝐷) |
6 | | fucco.f |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) |
7 | 3 | natrcl 16433 |
. . . . . . . 8
⊢ (𝑅 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
9 | 8 | simpld 474 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
10 | | funcrcl 16346 |
. . . . . 6
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
12 | 11 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
13 | 11 | simprd 478 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
14 | | fucco.x |
. . . 4
⊢ ∙ =
(comp‘𝑄) |
15 | 1, 2, 3, 4, 5, 12,
13, 14 | fuccofval 16442 |
. . 3
⊢ (𝜑 → ∙ = (𝑣 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)), ℎ ∈ (𝐶 Func 𝐷) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
16 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝑣) ∈ V |
17 | 16 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → (1st ‘𝑣) ∈ V) |
18 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → 𝑣 = 〈𝐹, 𝐺〉) |
19 | 18 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → (1st ‘𝑣) = (1st
‘〈𝐹, 𝐺〉)) |
20 | | op1stg 7071 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
21 | 8, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
23 | 19, 22 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → (1st ‘𝑣) = 𝐹) |
24 | | fvex 6113 |
. . . . . 6
⊢
(2nd ‘𝑣) ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd ‘𝑣) ∈ V) |
26 | 18 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → 𝑣 = 〈𝐹, 𝐺〉) |
27 | 26 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd ‘𝑣) = (2nd
‘〈𝐹, 𝐺〉)) |
28 | | op2ndg 7072 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
29 | 8, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
30 | 29 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
31 | 27, 30 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd ‘𝑣) = 𝐺) |
32 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
33 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → ℎ = 𝐻) |
34 | 33 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ℎ = 𝐻) |
35 | 32, 34 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝑁ℎ) = (𝐺𝑁𝐻)) |
36 | | simplr 788 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
37 | 36, 32 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑁𝑔) = (𝐹𝑁𝐺)) |
38 | 36 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st ‘𝑓) = (1st ‘𝐹)) |
39 | 38 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st ‘𝑓)‘𝑥) = ((1st ‘𝐹)‘𝑥)) |
40 | 32 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st ‘𝑔) = (1st ‘𝐺)) |
41 | 40 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st ‘𝑔)‘𝑥) = ((1st ‘𝐺)‘𝑥)) |
42 | 39, 41 | opeq12d 4348 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) |
43 | 34 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st ‘ℎ) = (1st ‘𝐻)) |
44 | 43 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st ‘ℎ)‘𝑥) = ((1st ‘𝐻)‘𝑥)) |
45 | 42, 44 | oveq12d 6567 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (〈((1st
‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥)) = (〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))) |
46 | 45 | oveqd 6566 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)) = ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))) |
47 | 46 | mpteq2dv 4673 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥)))) |
48 | 35, 37, 47 | mpt2eq123dv 6615 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))))) |
49 | 25, 31, 48 | csbied2 3527 |
. . . 4
⊢ (((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) ∧ 𝑓 = 𝐹) → ⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))))) |
50 | 17, 23, 49 | csbied2 3527 |
. . 3
⊢ ((𝜑 ∧ (𝑣 = 〈𝐹, 𝐺〉 ∧ ℎ = 𝐻)) → ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))))) |
51 | | opelxpi 5072 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → 〈𝐹, 𝐺〉 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))) |
52 | 8, 51 | syl 17 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))) |
53 | | fucco.g |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (𝐺𝑁𝐻)) |
54 | 3 | natrcl 16433 |
. . . . 5
⊢ (𝑆 ∈ (𝐺𝑁𝐻) → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷))) |
55 | 53, 54 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷))) |
56 | 55 | simprd 478 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (𝐶 Func 𝐷)) |
57 | | ovex 6577 |
. . . . 5
⊢ (𝐺𝑁𝐻) ∈ V |
58 | | ovex 6577 |
. . . . 5
⊢ (𝐹𝑁𝐺) ∈ V |
59 | 57, 58 | mpt2ex 7136 |
. . . 4
⊢ (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥)))) ∈ V |
60 | 59 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥)))) ∈ V) |
61 | 15, 50, 52, 56, 60 | ovmpt2d 6686 |
. 2
⊢ (𝜑 → (〈𝐹, 𝐺〉 ∙ 𝐻) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))))) |
62 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → 𝑏 = 𝑆) |
63 | 62 | fveq1d 6105 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → (𝑏‘𝑥) = (𝑆‘𝑥)) |
64 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → 𝑎 = 𝑅) |
65 | 64 | fveq1d 6105 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → (𝑎‘𝑥) = (𝑅‘𝑥)) |
66 | 63, 65 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥)) = ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑅‘𝑥))) |
67 | 66 | mpteq2dv 4673 |
. 2
⊢ ((𝜑 ∧ (𝑏 = 𝑆 ∧ 𝑎 = 𝑅)) → (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑅‘𝑥)))) |
68 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐶)
∈ V |
69 | 4, 68 | eqeltri 2684 |
. . . 4
⊢ 𝐴 ∈ V |
70 | 69 | mptex 6390 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑅‘𝑥))) ∈ V |
71 | 70 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑅‘𝑥))) ∈ V) |
72 | 61, 67, 53, 6, 71 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝑆(〈𝐹, 𝐺〉 ∙ 𝐻)𝑅) = (𝑥 ∈ 𝐴 ↦ ((𝑆‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 · ((1st
‘𝐻)‘𝑥))(𝑅‘𝑥)))) |