Step |
Hyp |
Ref |
Expression |
1 |
|
fucco.q |
⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 ) |
2 |
|
fucco.n |
⊢ 𝑁 = ( 𝐶 Nat 𝐷 ) |
3 |
|
fucco.a |
⊢ 𝐴 = ( Base ‘ 𝐶 ) |
4 |
|
fucco.o |
⊢ · = ( comp ‘ 𝐷 ) |
5 |
|
fucco.x |
⊢ ∙ = ( comp ‘ 𝑄 ) |
6 |
|
fucco.f |
⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) ) |
7 |
|
fucco.g |
⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) ) |
8 |
|
eqid |
⊢ ( 𝐶 Func 𝐷 ) = ( 𝐶 Func 𝐷 ) |
9 |
2
|
natrcl |
⊢ ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) ) |
10 |
6 9
|
syl |
⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) ) |
11 |
10
|
simpld |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) |
12 |
|
funcrcl |
⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) |
13 |
11 12
|
syl |
⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) ) |
14 |
13
|
simpld |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
15 |
13
|
simprd |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
16 |
1 8 2 3 4 14 15 5
|
fuccofval |
⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) |
17 |
|
fvexd |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ( 1st ‘ 𝑣 ) ∈ V ) |
18 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → 𝑣 = 〈 𝐹 , 𝐺 〉 ) |
19 |
18
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ 〈 𝐹 , 𝐺 〉 ) ) |
20 |
|
op1stg |
⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐹 ) |
21 |
10 20
|
syl |
⊢ ( 𝜑 → ( 1st ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐹 ) |
22 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ( 1st ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐹 ) |
23 |
19 22
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ( 1st ‘ 𝑣 ) = 𝐹 ) |
24 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd ‘ 𝑣 ) ∈ V ) |
25 |
18
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → 𝑣 = 〈 𝐹 , 𝐺 〉 ) |
26 |
25
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ 〈 𝐹 , 𝐺 〉 ) ) |
27 |
|
op2ndg |
⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 2nd ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐺 ) |
28 |
10 27
|
syl |
⊢ ( 𝜑 → ( 2nd ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐺 ) |
29 |
28
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd ‘ 〈 𝐹 , 𝐺 〉 ) = 𝐺 ) |
30 |
26 29
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd ‘ 𝑣 ) = 𝐺 ) |
31 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 ) |
32 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ℎ = 𝐻 ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ℎ = 𝐻 ) |
34 |
31 33
|
oveq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 𝑁 ℎ ) = ( 𝐺 𝑁 𝐻 ) ) |
35 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 ) |
36 |
35 31
|
oveq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 𝑁 𝑔 ) = ( 𝐹 𝑁 𝐺 ) ) |
37 |
35
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) ) |
38 |
37
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) |
39 |
31
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st ‘ 𝑔 ) = ( 1st ‘ 𝐺 ) ) |
40 |
39
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) ) |
41 |
38 40
|
opeq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 = 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 ) |
42 |
33
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st ‘ ℎ ) = ( 1st ‘ 𝐻 ) ) |
43 |
42
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st ‘ ℎ ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) |
44 |
41 43
|
oveq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) = ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ) |
45 |
44
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) |
46 |
45
|
mpteq2dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) |
47 |
34 36 46
|
mpoeq123dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) |
48 |
24 30 47
|
csbied2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) |
49 |
17 23 48
|
csbied2 |
⊢ ( ( 𝜑 ∧ ( 𝑣 = 〈 𝐹 , 𝐺 〉 ∧ ℎ = 𝐻 ) ) → ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) |
50 |
|
opelxpi |
⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → 〈 𝐹 , 𝐺 〉 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ) |
51 |
10 50
|
syl |
⊢ ( 𝜑 → 〈 𝐹 , 𝐺 〉 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ) |
52 |
2
|
natrcl |
⊢ ( 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) ) |
53 |
7 52
|
syl |
⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) ) |
54 |
53
|
simprd |
⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) |
55 |
|
ovex |
⊢ ( 𝐺 𝑁 𝐻 ) ∈ V |
56 |
|
ovex |
⊢ ( 𝐹 𝑁 𝐺 ) ∈ V |
57 |
55 56
|
mpoex |
⊢ ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V |
58 |
57
|
a1i |
⊢ ( 𝜑 → ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V ) |
59 |
16 49 51 54 58
|
ovmpod |
⊢ ( 𝜑 → ( 〈 𝐹 , 𝐺 〉 ∙ 𝐻 ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) |
60 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → 𝑏 = 𝑆 ) |
61 |
60
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑏 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) ) |
62 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → 𝑎 = 𝑅 ) |
63 |
62
|
fveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) ) |
64 |
61 63
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) |
65 |
64
|
mpteq2dv |
⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ) |
66 |
3
|
fvexi |
⊢ 𝐴 ∈ V |
67 |
66
|
mptex |
⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ V |
68 |
67
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ V ) |
69 |
59 65 7 6 68
|
ovmpod |
⊢ ( 𝜑 → ( 𝑆 ( 〈 𝐹 , 𝐺 〉 ∙ 𝐻 ) 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝐺 ) ‘ 𝑥 ) 〉 · ( ( 1st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ) |