Step |
Hyp |
Ref |
Expression |
1 |
|
xpchomfval.t |
⊢ 𝑇 = ( 𝐶 ×c 𝐷 ) |
2 |
|
xpchomfval.y |
⊢ 𝐵 = ( Base ‘ 𝑇 ) |
3 |
|
xpchomfval.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
4 |
|
xpchomfval.j |
⊢ 𝐽 = ( Hom ‘ 𝐷 ) |
5 |
|
xpchomfval.k |
⊢ 𝐾 = ( Hom ‘ 𝑇 ) |
6 |
|
xpchom.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
7 |
|
xpchom.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
8 |
|
simpl |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → 𝑢 = 𝑋 ) |
9 |
8
|
fveq2d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑋 ) ) |
10 |
|
simpr |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → 𝑣 = 𝑌 ) |
11 |
10
|
fveq2d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑌 ) ) |
12 |
9 11
|
oveq12d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) ) |
13 |
8
|
fveq2d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 2nd ‘ 𝑢 ) = ( 2nd ‘ 𝑋 ) ) |
14 |
10
|
fveq2d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ 𝑌 ) ) |
15 |
13 14
|
oveq12d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) = ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) |
16 |
12 15
|
xpeq12d |
⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) ) |
17 |
1 2 3 4 5
|
xpchomfval |
⊢ 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) ) ) |
18 |
|
ovex |
⊢ ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) ∈ V |
19 |
|
ovex |
⊢ ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ∈ V |
20 |
18 19
|
xpex |
⊢ ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) ∈ V |
21 |
16 17 20
|
ovmpoa |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) ) |
22 |
6 7 21
|
syl2anc |
⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) ) |