Theorem xpsaddlem

Description: Lemma for xpsadd and xpsmul . (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsval.x	$$⊢X={\mathrm{Base}}_R$$
	xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsval.1	$$⊢\phi \to R\in V$$
	xpsval.2	$$⊢\phi \to S\in W$$
	xpsadd.3	$$⊢\phi \to A\in X$$
	xpsadd.4	$$⊢\phi \to B\in Y$$
	xpsadd.5	$$⊢\phi \to C\in X$$
	xpsadd.6	$$⊢\phi \to D\in Y$$
	xpsadd.7	$$⊢\phi \to A\underset{\dot{}}{·}C\in X$$
	xpsadd.8	$$⊢\phi \to B\underset{\dot{}}{\times }D\in Y$$
	xpsaddlem.m	$$⊢\underset{\dot{}}{·}=E\left(R\right)$$
	xpsaddlem.n	$$⊢\underset{\dot{}}{\times }=E\left(S\right)$$
	xpsaddlem.p	$$⊢\underset{\dot{}}{\bullet }=E\left(T\right)$$
	xpsaddlem.f	$$⊢F=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
	xpsaddlem.u	$$⊢U=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
	xpsaddlem.1	$$⊢\left(\phi \wedge \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in \mathrm{ran}F\wedge \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in \mathrm{ran}F\right)\to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)\underset{\dot{}}{\bullet }{F}^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)$$
	xpsaddlem.2	$$⊢\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}\wedge \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in {\mathrm{Base}}_U\wedge \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in {\mathrm{Base}}_U\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)\right)$$
Assertion	xpsaddlem	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{\bullet }⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$

Proof

Step	Hyp	Ref	Expression
1		xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsval.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsval.1	$$⊢\phi \to R\in V$$
5		xpsval.2	$$⊢\phi \to S\in W$$
6		xpsadd.3	$$⊢\phi \to A\in X$$
7		xpsadd.4	$$⊢\phi \to B\in Y$$
8		xpsadd.5	$$⊢\phi \to C\in X$$
9		xpsadd.6	$$⊢\phi \to D\in Y$$
10		xpsadd.7	$$⊢\phi \to A\underset{\dot{}}{·}C\in X$$
11		xpsadd.8	$$⊢\phi \to B\underset{\dot{}}{\times }D\in Y$$
12		xpsaddlem.m	$$⊢\underset{\dot{}}{·}=E\left(R\right)$$
13		xpsaddlem.n	$$⊢\underset{\dot{}}{\times }=E\left(S\right)$$
14		xpsaddlem.p	$$⊢\underset{\dot{}}{\bullet }=E\left(T\right)$$
15		xpsaddlem.f	$$⊢F=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
16		xpsaddlem.u	$$⊢U=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
17		xpsaddlem.1	$$⊢\left(\phi \wedge \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in \mathrm{ran}F\wedge \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in \mathrm{ran}F\right)\to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)\underset{\dot{}}{\bullet }{F}^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)$$
18		xpsaddlem.2	$$⊢\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}\wedge \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in {\mathrm{Base}}_U\wedge \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in {\mathrm{Base}}_U\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)\right)$$
19		df-ov	$$⊢AFB=F\left(⟨A,B⟩\right)$$
20	15	xpsfval	$$⊢\left(A\in X\wedge B\in Y\right)\to AFB=\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}$$
21	6 7 20	syl2anc	$$⊢\phi \to AFB=\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}$$
22	19 21	syl5eqr	$$⊢\phi \to F\left(⟨A,B⟩\right)=\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}$$
23	6 7	opelxpd	$$⊢\phi \to ⟨A,B⟩\in \left(X\times Y\right)$$
24	15	xpsff1o2	$$⊢F:X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
25		f1of	$$⊢F:X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}F\to F:X\times Y⟶\mathrm{ran}F$$
26	24 25	ax-mp	$$⊢F:X\times Y⟶\mathrm{ran}F$$
27	26	ffvelrni	$$⊢⟨A,B⟩\in \left(X\times Y\right)\to F\left(⟨A,B⟩\right)\in \mathrm{ran}F$$
28	23 27	syl	$$⊢\phi \to F\left(⟨A,B⟩\right)\in \mathrm{ran}F$$
29	22 28	eqeltrrd	$$⊢\phi \to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in \mathrm{ran}F$$
30		df-ov	$$⊢CFD=F\left(⟨C,D⟩\right)$$
31	15	xpsfval	$$⊢\left(C\in X\wedge D\in Y\right)\to CFD=\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}$$
32	8 9 31	syl2anc	$$⊢\phi \to CFD=\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}$$
33	30 32	syl5eqr	$$⊢\phi \to F\left(⟨C,D⟩\right)=\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}$$
34	8 9	opelxpd	$$⊢\phi \to ⟨C,D⟩\in \left(X\times Y\right)$$
35	26	ffvelrni	$$⊢⟨C,D⟩\in \left(X\times Y\right)\to F\left(⟨C,D⟩\right)\in \mathrm{ran}F$$
36	34 35	syl	$$⊢\phi \to F\left(⟨C,D⟩\right)\in \mathrm{ran}F$$
37	33 36	eqeltrrd	$$⊢\phi \to \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in \mathrm{ran}F$$
38	29 37 17	mpd3an23	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)\underset{\dot{}}{\bullet }{F}^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)$$
39		f1ocnvfv	$$⊢\left(F:X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}F\wedge ⟨A,B⟩\in \left(X\times Y\right)\right)\to \left(F\left(⟨A,B⟩\right)=\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)=⟨A,B⟩\right)$$
40	24 23 39	sylancr	$$⊢\phi \to \left(F\left(⟨A,B⟩\right)=\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)=⟨A,B⟩\right)$$
41	22 40	mpd	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)=⟨A,B⟩$$
42		f1ocnvfv	$$⊢\left(F:X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}F\wedge ⟨C,D⟩\in \left(X\times Y\right)\right)\to \left(F\left(⟨C,D⟩\right)=\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=⟨C,D⟩\right)$$
43	24 34 42	sylancr	$$⊢\phi \to \left(F\left(⟨C,D⟩\right)=\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=⟨C,D⟩\right)$$
44	33 43	mpd	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=⟨C,D⟩$$
45	41 44	oveq12d	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\right)\underset{\dot{}}{\bullet }{F}^{-1}\left(\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=⟨A,B⟩\underset{\dot{}}{\bullet }⟨C,D⟩$$
46		iftrue	$$⊢k=\varnothing \to if\left(k=\varnothing ,R,S\right)=R$$
47	46	fveq2d	$$⊢k=\varnothing \to E\left(if\left(k=\varnothing ,R,S\right)\right)=E\left(R\right)$$
48	47 12	eqtr4di	$$⊢k=\varnothing \to E\left(if\left(k=\varnothing ,R,S\right)\right)=\underset{\dot{}}{·}$$
49		iftrue	$$⊢k=\varnothing \to if\left(k=\varnothing ,A,B\right)=A$$
50		iftrue	$$⊢k=\varnothing \to if\left(k=\varnothing ,C,D\right)=C$$
51	48 49 50	oveq123d	$$⊢k=\varnothing \to if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)=A\underset{\dot{}}{·}C$$
52		iftrue	$$⊢k=\varnothing \to if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)=A\underset{\dot{}}{·}C$$
53	51 52	eqtr4d	$$⊢k=\varnothing \to if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)=if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)$$
54		iffalse	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,R,S\right)=S$$
55	54	fveq2d	$$⊢\neg k=\varnothing \to E\left(if\left(k=\varnothing ,R,S\right)\right)=E\left(S\right)$$
56	55 13	eqtr4di	$$⊢\neg k=\varnothing \to E\left(if\left(k=\varnothing ,R,S\right)\right)=\underset{\dot{}}{\times }$$
57		iffalse	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,A,B\right)=B$$
58		iffalse	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,C,D\right)=D$$
59	56 57 58	oveq123d	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)=B\underset{\dot{}}{\times }D$$
60		iffalse	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)=B\underset{\dot{}}{\times }D$$
61	59 60	eqtr4d	$$⊢\neg k=\varnothing \to if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)=if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)$$
62	53 61	pm2.61i	$$⊢if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)=if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)$$
63	4	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to R\in V$$
64	5	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to S\in W$$
65		simpr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to k\in 2_{𝑜}$$
66		fvprif	$$⊢\left(R\in V\wedge S\in W\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)$$
67	63 64 65 66	syl3anc	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)$$
68	67	fveq2d	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)=E\left(if\left(k=\varnothing ,R,S\right)\right)$$
69	6	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to A\in X$$
70	7	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to B\in Y$$
71		fvprif	$$⊢\left(A\in X\wedge B\in Y\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)=if\left(k=\varnothing ,A,B\right)$$
72	69 70 65 71	syl3anc	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)=if\left(k=\varnothing ,A,B\right)$$
73	8	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to C\in X$$
74	9	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to D\in Y$$
75		fvprif	$$⊢\left(C\in X\wedge D\in Y\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)=if\left(k=\varnothing ,C,D\right)$$
76	73 74 65 75	syl3anc	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)=if\left(k=\varnothing ,C,D\right)$$
77	68 72 76	oveq123d	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)=if\left(k=\varnothing ,A,B\right)E\left(if\left(k=\varnothing ,R,S\right)\right)if\left(k=\varnothing ,C,D\right)$$
78	10	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to A\underset{\dot{}}{·}C\in X$$
79	11	adantr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to B\underset{\dot{}}{\times }D\in Y$$
80		fvprif	$$⊢\left(A\underset{\dot{}}{·}C\in X\wedge B\underset{\dot{}}{\times }D\in Y\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)=if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)$$
81	78 79 65 80	syl3anc	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)=if\left(k=\varnothing ,A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D\right)$$
82	62 77 81	3eqtr4a	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)$$
83	82	mpteq2dva	$$⊢\phi \to \left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)\right)=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)\right)$$
84		fnpr2o	$$⊢\left(R\in V\wedge S\in W\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}$$
85	4 5 84	syl2anc	$$⊢\phi \to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}$$
86		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
87	1 2 3 4 5 15 86 16	xpsrnbas	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_U$$
88	29 87	eleqtrd	$$⊢\phi \to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\in {\mathrm{Base}}_U$$
89	37 87	eleqtrd	$$⊢\phi \to \left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\in {\mathrm{Base}}_U$$
90	85 88 89 18	syl3anc	$$⊢\phi \to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}\left(k\right)E\left(\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\left(k\right)\right)$$
91		fnpr2o	$$⊢\left(A\underset{\dot{}}{·}C\in X\wedge B\underset{\dot{}}{\times }D\in Y\right)\to \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}Fn{2}_{𝑜}$$
92	10 11 91	syl2anc	$$⊢\phi \to \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}Fn{2}_{𝑜}$$
93		dffn5	$$⊢\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}Fn{2}_{𝑜}\leftrightarrow \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)\right)$$
94	92 93	sylib	$$⊢\phi \to \left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}=\left(k\in 2_{𝑜}⟼\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\left(k\right)\right)$$
95	83 90 94	3eqtr4d	$$⊢\phi \to \left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}$$
96	95	fveq2d	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=F^{-1}\left(\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\right)$$
97		df-ov	$$⊢\left(A\underset{\dot{}}{·}C\right)F\left(B\underset{\dot{}}{\times }D\right)=F\left(⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)$$
98	15	xpsfval	$$⊢\left(A\underset{\dot{}}{·}C\in X\wedge B\underset{\dot{}}{\times }D\in Y\right)\to \left(A\underset{\dot{}}{·}C\right)F\left(B\underset{\dot{}}{\times }D\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}$$
99	10 11 98	syl2anc	$$⊢\phi \to \left(A\underset{\dot{}}{·}C\right)F\left(B\underset{\dot{}}{\times }D\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}$$
100	97 99	syl5eqr	$$⊢\phi \to F\left(⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}$$
101	10 11	opelxpd	$$⊢\phi \to ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\in \left(X\times Y\right)$$
102		f1ocnvfv	$$⊢\left(F:X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}F\wedge ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\in \left(X\times Y\right)\right)\to \left(F\left(⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\right)=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)$$
103	24 101 102	sylancr	$$⊢\phi \to \left(F\left(⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)=\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\to F^{-1}\left(\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\right)=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\right)$$
104	100 103	mpd	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A\underset{\dot{}}{·}C⟩,⟨1_{𝑜},B\underset{\dot{}}{\times }D⟩\right\}\right)=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$
105	96 104	eqtrd	$$⊢\phi \to F^{-1}\left(\left\{⟨\varnothing ,A⟩,⟨1_{𝑜},B⟩\right\}E\left(U\right)\left\{⟨\varnothing ,C⟩,⟨1_{𝑜},D⟩\right\}\right)=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$
106	38 45 105	3eqtr3d	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{\bullet }⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$