Theorem tposcurf1

Description: Value of the object part of the transposed curry functor. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf1.g	No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
	tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
	tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	tposcurf1.x	$$⊢\phi \to X\in A$$
	tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
	tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
	tposcurf1.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	tposcurf1.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	tposcurf1	$$⊢\phi \to K=⟨\left(y\in B⟼y{1}^{st}\left(F\right)X\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼g\left(⟨y,X⟩2^{nd}\left(F\right)⟨z,X⟩\right)\underset{\dot{}}{1}\left(X\right)\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.g	Could not format ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
2		tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
3		tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
6		tposcurf1.x	$$⊢\phi \to X\in A$$
7		tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
8		tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
9		tposcurf1.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
10		tposcurf1.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
11	1	fveq2d	Could not format ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) with typecode |-
12	11	fveq1d	Could not format ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) : No typesetting found for |- ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) with typecode |-
13		eqid	Could not format ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) with typecode |-
14		eqidd	Could not format ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) with typecode |-
15	3 4 5 14	cofuswapfcl	Could not format ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) with typecode |-
16		eqid	Could not format ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) : No typesetting found for |- ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) with typecode |-
17	13 2 3 4 15 8 6 16 9 10	curf1	Could not format ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. ) with typecode |-
18	7 12 17	3eqtrd	Could not format ( ph -> K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. ) : No typesetting found for |- ( ph -> K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. ) with typecode |-
19	8	fvexi	$$⊢B\in \mathrm{V}$$
20	19	mptex	Could not format ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) e. _V : No typesetting found for |- ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) e. _V with typecode |-
21	19 19	mpoex	Could not format ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) e. _V : No typesetting found for |- ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) e. _V with typecode |-
22	20 21	op1std	Could not format ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) ) : No typesetting found for |- ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) ) with typecode |-
23	18 22	syl	Could not format ( ph -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) ) : No typesetting found for |- ( ph -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) ) with typecode |-
24		ovexd	Could not format ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) e. _V ) : No typesetting found for |- ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) e. _V ) with typecode |-
25	23 24	fvmpt2d	Could not format ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) : No typesetting found for |- ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) with typecode |-
26	1	adantr	Could not format ( ( ph /\ y e. B ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ( ph /\ y e. B ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
27	3	adantr	$$⊢\left(\phi \wedge y\in B\right)\to C\in \mathrm{Cat}$$
28	4	adantr	$$⊢\left(\phi \wedge y\in B\right)\to D\in \mathrm{Cat}$$
29	5	adantr	$$⊢\left(\phi \wedge y\in B\right)\to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
30	6	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in A$$
31	7	adantr	$$⊢\left(\phi \wedge y\in B\right)\to K=1^{st}\left(G\right)\left(X\right)$$
32		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
33	26 2 27 28 29 30 31 8 32	tposcurf11	$$⊢\left(\phi \wedge y\in B\right)\to 1^{st}\left(K\right)\left(y\right)=y{1}^{st}\left(F\right)X$$
34	25 33	eqtr3d	Could not format ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) = ( y ( 1st ` F ) X ) ) : No typesetting found for |- ( ( ph /\ y e. B ) -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) = ( y ( 1st ` F ) X ) ) with typecode |-
35	34	mpteq2dva	Could not format ( ph -> ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) = ( y e. B |-> ( y ( 1st ` F ) X ) ) ) : No typesetting found for |- ( ph -> ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) = ( y e. B |-> ( y ( 1st ` F ) X ) ) ) with typecode |-
36	20 21	op2ndd	Could not format ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) ) : No typesetting found for |- ( K = <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) ) with typecode |-
37	18 36	syl	Could not format ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) ) with typecode |-
38		ovex	$$⊢yJz\in \mathrm{V}$$
39	38	mptex	Could not format ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V : No typesetting found for |- ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V with typecode |-
40	39	a1i	Could not format ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V ) : No typesetting found for |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) e. _V ) with typecode |-
41	37 40	ovmpt4d	Could not format ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( 2nd ` K ) z ) = ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) : No typesetting found for |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( 2nd ` K ) z ) = ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) with typecode |-
42		ovexd	Could not format ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) e. _V ) : No typesetting found for |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) e. _V ) with typecode |-
43	41 42	fvmpt2d	Could not format ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) : No typesetting found for |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) with typecode |-
44	1	ad2antrr	Could not format ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
45	3	ad2antrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to C\in \mathrm{Cat}$$
46	4	ad2antrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to D\in \mathrm{Cat}$$
47	5	ad2antrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
48	6	ad2antrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to X\in A$$
49	7	ad2antrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to K=1^{st}\left(G\right)\left(X\right)$$
50		simplrl	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to y\in B$$
51		simplrr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to z\in B$$
52		simpr	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to g\in \left(yJz\right)$$
53	44 2 45 46 47 48 49 8 50 9 10 51 52	tposcurf12	$$⊢\left(\left(\phi \wedge \left(y\in B\wedge z\in B\right)\right)\wedge g\in \left(yJz\right)\right)\to \left(y{2}^{nd}\left(K\right)z\right)\left(g\right)=g\left(⟨y,X⟩2^{nd}\left(F\right)⟨z,X⟩\right)\underset{\dot{}}{1}\left(X\right)$$
54	43 53	eqtr3d	Could not format ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) = ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) : No typesetting found for |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y J z ) ) -> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) = ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) with typecode |-
55	54	mpteq2dva	Could not format ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) : No typesetting found for |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) with typecode |-
56	55	3impb	Could not format ( ( ph /\ y e. B /\ z e. B ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) : No typesetting found for |- ( ( ph /\ y e. B /\ z e. B ) -> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) = ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) with typecode |-
57	56	mpoeq3dva	Could not format ( ph -> ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) ) : No typesetting found for |- ( ph -> ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) = ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) ) with typecode |-
58	35 57	opeq12d	Could not format ( ph -> <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. = <. ( y e. B |-> ( y ( 1st ` F ) X ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) >. ) : No typesetting found for |- ( ph -> <. ( y e. B |-> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , z >. ) g ) ) ) >. = <. ( y e. B |-> ( y ( 1st ` F ) X ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( g ( <. y , X >. ( 2nd ` F ) <. z , X >. ) ( .1. ` X ) ) ) ) >. ) with typecode |-
59	18 58	eqtrd	$$⊢\phi \to K=⟨\left(y\in B⟼y{1}^{st}\left(F\right)X\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼g\left(⟨y,X⟩2^{nd}\left(F\right)⟨z,X⟩\right)\underset{\dot{}}{1}\left(X\right)\right)\right)⟩$$