MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpcval Structured version   Visualization version   GIF version

Theorem xpcval 18139
Description: Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
Hypotheses
Ref Expression
xpcval.t 𝑇 = (𝐢 Γ—c 𝐷)
xpcval.x 𝑋 = (Baseβ€˜πΆ)
xpcval.y π‘Œ = (Baseβ€˜π·)
xpcval.h 𝐻 = (Hom β€˜πΆ)
xpcval.j 𝐽 = (Hom β€˜π·)
xpcval.o1 Β· = (compβ€˜πΆ)
xpcval.o2 βˆ™ = (compβ€˜π·)
xpcval.c (πœ‘ β†’ 𝐢 ∈ 𝑉)
xpcval.d (πœ‘ β†’ 𝐷 ∈ π‘Š)
xpcval.b (πœ‘ β†’ 𝐡 = (𝑋 Γ— π‘Œ))
xpcval.k (πœ‘ β†’ 𝐾 = (𝑒 ∈ 𝐡, 𝑣 ∈ 𝐡 ↦ (((1st β€˜π‘’)𝐻(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£)))))
xpcval.o (πœ‘ β†’ 𝑂 = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ 𝐡 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)𝐾𝑦), 𝑓 ∈ (πΎβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)))
Assertion
Ref Expression
xpcval (πœ‘ β†’ 𝑇 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
Distinct variable groups:   𝑓,𝑔,𝑒,𝑣,π‘₯,𝑦,𝐡   πœ‘,𝑓,𝑔,𝑒,𝑣,π‘₯,𝑦   𝐢,𝑓,𝑔,𝑒,𝑣,π‘₯,𝑦   𝐷,𝑓,𝑔,𝑒,𝑣,π‘₯,𝑦   𝑓,𝐾,𝑔,π‘₯,𝑦
Allowed substitution hints:   βˆ™ (π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝑇(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   Β· (π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝐻(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝐽(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝐾(𝑣,𝑒)   𝑂(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝑉(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   π‘Š(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   𝑋(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)   π‘Œ(π‘₯,𝑦,𝑣,𝑒,𝑓,𝑔)

Proof of Theorem xpcval
Dummy variables 𝑏 β„Ž π‘Ÿ 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpcval.t . 2 𝑇 = (𝐢 Γ—c 𝐷)
2 df-xpc 18134 . . . 4 Γ—c = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩})
32a1i 11 . . 3 (πœ‘ β†’ Γ—c = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩}))
4 fvex 6897 . . . . . 6 (Baseβ€˜π‘Ÿ) ∈ V
5 fvex 6897 . . . . . 6 (Baseβ€˜π‘ ) ∈ V
64, 5xpex 7736 . . . . 5 ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) ∈ V
76a1i 11 . . . 4 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) ∈ V)
8 simprl 768 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ π‘Ÿ = 𝐢)
98fveq2d 6888 . . . . . . 7 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜πΆ))
10 xpcval.x . . . . . . 7 𝑋 = (Baseβ€˜πΆ)
119, 10eqtr4di 2784 . . . . . 6 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ (Baseβ€˜π‘Ÿ) = 𝑋)
12 simprr 770 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ 𝑠 = 𝐷)
1312fveq2d 6888 . . . . . . 7 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ (Baseβ€˜π‘ ) = (Baseβ€˜π·))
14 xpcval.y . . . . . . 7 π‘Œ = (Baseβ€˜π·)
1513, 14eqtr4di 2784 . . . . . 6 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ (Baseβ€˜π‘ ) = π‘Œ)
1611, 15xpeq12d 5700 . . . . 5 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) = (𝑋 Γ— π‘Œ))
17 xpcval.b . . . . . 6 (πœ‘ β†’ 𝐡 = (𝑋 Γ— π‘Œ))
1817adantr 480 . . . . 5 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ 𝐡 = (𝑋 Γ— π‘Œ))
1916, 18eqtr4d 2769 . . . 4 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) = 𝐡)
20 vex 3472 . . . . . . 7 𝑏 ∈ V
2120, 20mpoex 8062 . . . . . 6 (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) ∈ V
2221a1i 11 . . . . 5 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) ∈ V)
23 simpr 484 . . . . . . 7 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ 𝑏 = 𝐡)
24 simplrl 774 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ π‘Ÿ = 𝐢)
2524fveq2d 6888 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘Ÿ) = (Hom β€˜πΆ))
26 xpcval.h . . . . . . . . . 10 𝐻 = (Hom β€˜πΆ)
2725, 26eqtr4di 2784 . . . . . . . . 9 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘Ÿ) = 𝐻)
2827oveqd 7421 . . . . . . . 8 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ ((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) = ((1st β€˜π‘’)𝐻(1st β€˜π‘£)))
29 simplrr 775 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ 𝑠 = 𝐷)
3029fveq2d 6888 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘ ) = (Hom β€˜π·))
31 xpcval.j . . . . . . . . . 10 𝐽 = (Hom β€˜π·)
3230, 31eqtr4di 2784 . . . . . . . . 9 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘ ) = 𝐽)
3332oveqd 7421 . . . . . . . 8 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)) = ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£)))
3428, 33xpeq12d 5700 . . . . . . 7 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£))) = (((1st β€˜π‘’)𝐻(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£))))
3523, 23, 34mpoeq123dv 7479 . . . . . 6 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) = (𝑒 ∈ 𝐡, 𝑣 ∈ 𝐡 ↦ (((1st β€˜π‘’)𝐻(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£)))))
36 xpcval.k . . . . . . 7 (πœ‘ β†’ 𝐾 = (𝑒 ∈ 𝐡, 𝑣 ∈ 𝐡 ↦ (((1st β€˜π‘’)𝐻(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£)))))
3736ad2antrr 723 . . . . . 6 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ 𝐾 = (𝑒 ∈ 𝐡, 𝑣 ∈ 𝐡 ↦ (((1st β€˜π‘’)𝐻(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)𝐽(2nd β€˜π‘£)))))
3835, 37eqtr4d 2769 . . . . 5 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) = 𝐾)
39 simplr 766 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ 𝑏 = 𝐡)
4039opeq2d 4875 . . . . . 6 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ⟨(Baseβ€˜ndx), π‘βŸ© = ⟨(Baseβ€˜ndx), 𝐡⟩)
41 simpr 484 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ β„Ž = 𝐾)
4241opeq2d 4875 . . . . . 6 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ⟨(Hom β€˜ndx), β„ŽβŸ© = ⟨(Hom β€˜ndx), 𝐾⟩)
4339, 39xpeq12d 5700 . . . . . . . . 9 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (𝑏 Γ— 𝑏) = (𝐡 Γ— 𝐡))
4441oveqd 7421 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ((2nd β€˜π‘₯)β„Žπ‘¦) = ((2nd β€˜π‘₯)𝐾𝑦))
4541fveq1d 6886 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (β„Žβ€˜π‘₯) = (πΎβ€˜π‘₯))
4624adantr 480 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ π‘Ÿ = 𝐢)
4746fveq2d 6888 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (compβ€˜π‘Ÿ) = (compβ€˜πΆ))
48 xpcval.o1 . . . . . . . . . . . . . 14 Β· = (compβ€˜πΆ)
4947, 48eqtr4di 2784 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (compβ€˜π‘Ÿ) = Β· )
5049oveqd 7421 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦)) = (⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦)))
5150oveqd 7421 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)) = ((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)))
5229adantr 480 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ 𝑠 = 𝐷)
5352fveq2d 6888 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (compβ€˜π‘ ) = (compβ€˜π·))
54 xpcval.o2 . . . . . . . . . . . . . 14 βˆ™ = (compβ€˜π·)
5553, 54eqtr4di 2784 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (compβ€˜π‘ ) = βˆ™ )
5655oveqd 7421 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦)) = (⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦)))
5756oveqd 7421 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“)) = ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“)))
5851, 57opeq12d 4876 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩ = ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)
5944, 45, 58mpoeq123dv 7479 . . . . . . . . 9 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩) = (𝑔 ∈ ((2nd β€˜π‘₯)𝐾𝑦), 𝑓 ∈ (πΎβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))
6043, 39, 59mpoeq123dv 7479 . . . . . . . 8 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)) = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ 𝐡 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)𝐾𝑦), 𝑓 ∈ (πΎβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)))
61 xpcval.o . . . . . . . . 9 (πœ‘ β†’ 𝑂 = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ 𝐡 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)𝐾𝑦), 𝑓 ∈ (πΎβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)))
6261ad3antrrr 727 . . . . . . . 8 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ 𝑂 = (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ 𝐡 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)𝐾𝑦), 𝑓 ∈ (πΎβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩ Β· (1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩ βˆ™ (2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)))
6360, 62eqtr4d 2769 . . . . . . 7 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)) = 𝑂)
6463opeq2d 4875 . . . . . 6 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩ = ⟨(compβ€˜ndx), π‘‚βŸ©)
6540, 42, 64tpeq123d 4747 . . . . 5 ((((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) ∧ β„Ž = 𝐾) β†’ {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
6622, 38, 65csbied2 3928 . . . 4 (((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐡) β†’ ⦋(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
677, 19, 66csbied2 3928 . . 3 ((πœ‘ ∧ (π‘Ÿ = 𝐢 ∧ 𝑠 = 𝐷)) β†’ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
68 xpcval.c . . . 4 (πœ‘ β†’ 𝐢 ∈ 𝑉)
6968elexd 3489 . . 3 (πœ‘ β†’ 𝐢 ∈ V)
70 xpcval.d . . . 4 (πœ‘ β†’ 𝐷 ∈ π‘Š)
7170elexd 3489 . . 3 (πœ‘ β†’ 𝐷 ∈ V)
72 tpex 7730 . . . 4 {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©} ∈ V
7372a1i 11 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©} ∈ V)
743, 67, 69, 71, 73ovmpod 7555 . 2 (πœ‘ β†’ (𝐢 Γ—c 𝐷) = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
751, 74eqtrid 2778 1 (πœ‘ β†’ 𝑇 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), 𝐾⟩, ⟨(compβ€˜ndx), π‘‚βŸ©})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  Vcvv 3468  β¦‹csb 3888  {ctp 4627  βŸ¨cop 4629   Γ— cxp 5667  β€˜cfv 6536  (class class class)co 7404   ∈ cmpo 7406  1st c1st 7969  2nd c2nd 7970  ndxcnx 17133  Basecbs 17151  Hom chom 17215  compcco 17216   Γ—c cxpc 18130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7971  df-2nd 7972  df-xpc 18134
This theorem is referenced by:  xpcbas  18140  xpchomfval  18141  xpccofval  18144  catcxpccl  18169  catcxpcclOLD  18170  xpcpropd  18171
  Copyright terms: Public domain W3C validator