fsplitfpar

Description: Merge two functions with a common argument in parallel. Combination of fsplit and fpar . (Contributed by AV, 3-Jan-2024)

	Ref	Expression
Hypotheses	fsplitfpar.h	\|- H = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( F o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( G o. ( 2nd \|` ( _V X. _V ) ) ) ) )
	fsplitfpar.s	\|- S = ( `' ( 1st \|` _I ) \|` A )
Assertion	fsplitfpar	\|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		fsplitfpar.h	\|- H = ( ( `' ( 1st \|` ( _V X. _V ) ) o. ( F o. ( 1st \|` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd \|` ( _V X. _V ) ) o. ( G o. ( 2nd \|` ( _V X. _V ) ) ) ) )
2		fsplitfpar.s	\|- S = ( `' ( 1st \|` _I ) \|` A )
3		fsplit	\|- `' ( 1st \|` _I ) = ( x e. _V \|-> <. x , x >. )
4	3	reseq1i	\|- ( `' ( 1st \|` _I ) \|` A ) = ( ( x e. _V \|-> <. x , x >. ) \|` A )
5	2 4	eqtri	\|- S = ( ( x e. _V \|-> <. x , x >. ) \|` A )
6	5	fveq1i	\|- ( S ` a ) = ( ( ( x e. _V \|-> <. x , x >. ) \|` A ) ` a )
7	6	a1i	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = ( ( ( x e. _V \|-> <. x , x >. ) \|` A ) ` a ) )
8		fvres	\|- ( a e. A -> ( ( ( x e. _V \|-> <. x , x >. ) \|` A ) ` a ) = ( ( x e. _V \|-> <. x , x >. ) ` a ) )
9		eqidd	\|- ( a e. A -> ( x e. _V \|-> <. x , x >. ) = ( x e. _V \|-> <. x , x >. ) )
10		id	\|- ( x = a -> x = a )
11	10 10	opeq12d	\|- ( x = a -> <. x , x >. = <. a , a >. )
12	11	adantl	\|- ( ( a e. A /\ x = a ) -> <. x , x >. = <. a , a >. )
13		elex	\|- ( a e. A -> a e. _V )
14		opex	\|- <. a , a >. e. _V
15	14	a1i	\|- ( a e. A -> <. a , a >. e. _V )
16	9 12 13 15	fvmptd	\|- ( a e. A -> ( ( x e. _V \|-> <. x , x >. ) ` a ) = <. a , a >. )
17	8 16	eqtrd	\|- ( a e. A -> ( ( ( x e. _V \|-> <. x , x >. ) \|` A ) ` a ) = <. a , a >. )
18	17	adantl	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( ( x e. _V \|-> <. x , x >. ) \|` A ) ` a ) = <. a , a >. )
19	7 18	eqtrd	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = <. a , a >. )
20	19	fveq2d	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = ( H ` <. a , a >. ) )
21		df-ov	\|- ( a H a ) = ( H ` <. a , a >. )
22	1	fpar	\|- ( ( F Fn A /\ G Fn A ) -> H = ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) )
23	22	adantr	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> H = ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) )
24		fveq2	\|- ( x = a -> ( F ` x ) = ( F ` a ) )
25	24	adantr	\|- ( ( x = a /\ y = a ) -> ( F ` x ) = ( F ` a ) )
26		fveq2	\|- ( y = a -> ( G ` y ) = ( G ` a ) )
27	26	adantl	\|- ( ( x = a /\ y = a ) -> ( G ` y ) = ( G ` a ) )
28	25 27	opeq12d	\|- ( ( x = a /\ y = a ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. )
29	28	adantl	\|- ( ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) /\ ( x = a /\ y = a ) ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. )
30		simpr	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> a e. A )
31		opex	\|- <. ( F ` a ) , ( G ` a ) >. e. _V
32	31	a1i	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. _V )
33	23 29 30 30 32	ovmpod	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( a H a ) = <. ( F ` a ) , ( G ` a ) >. )
34	21 33	eqtr3id	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` <. a , a >. ) = <. ( F ` a ) , ( G ` a ) >. )
35	20 34	eqtrd	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = <. ( F ` a ) , ( G ` a ) >. )
36		eqid	\|- ( a e. _V \|-> <. a , a >. ) = ( a e. _V \|-> <. a , a >. )
37	36	fnmpt	\|- ( A. a e. _V <. a , a >. e. _V -> ( a e. _V \|-> <. a , a >. ) Fn _V )
38	14	a1i	\|- ( a e. _V -> <. a , a >. e. _V )
39	37 38	mprg	\|- ( a e. _V \|-> <. a , a >. ) Fn _V
40		ssv	\|- A C_ _V
41		fnssres	\|- ( ( ( a e. _V \|-> <. a , a >. ) Fn _V /\ A C_ _V ) -> ( ( a e. _V \|-> <. a , a >. ) \|` A ) Fn A )
42	39 40 41	mp2an	\|- ( ( a e. _V \|-> <. a , a >. ) \|` A ) Fn A
43		fsplit	\|- `' ( 1st \|` _I ) = ( a e. _V \|-> <. a , a >. )
44	43	reseq1i	\|- ( `' ( 1st \|` _I ) \|` A ) = ( ( a e. _V \|-> <. a , a >. ) \|` A )
45	2 44	eqtri	\|- S = ( ( a e. _V \|-> <. a , a >. ) \|` A )
46	45	fneq1i	\|- ( S Fn A <-> ( ( a e. _V \|-> <. a , a >. ) \|` A ) Fn A )
47	42 46	mpbir	\|- S Fn A
48	47	a1i	\|- ( ( F Fn A /\ G Fn A ) -> S Fn A )
49		fvco2	\|- ( ( S Fn A /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) )
50	48 49	sylan	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) )
51		fveq2	\|- ( x = a -> ( G ` x ) = ( G ` a ) )
52	24 51	opeq12d	\|- ( x = a -> <. ( F ` x ) , ( G ` x ) >. = <. ( F ` a ) , ( G ` a ) >. )
53		eqid	\|- ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) = ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. )
54	52 53 31	fvmpt	\|- ( a e. A -> ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. )
55	54	adantl	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. )
56	35 50 55	3eqtr4d	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) )
57	56	ralrimiva	\|- ( ( F Fn A /\ G Fn A ) -> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) )
58		opex	\|- <. ( F ` x ) , ( G ` y ) >. e. _V
59	58	a1i	\|- ( ( ( F Fn A /\ G Fn A ) /\ ( x e. A /\ y e. A ) ) -> <. ( F ` x ) , ( G ` y ) >. e. _V )
60	59	ralrimivva	\|- ( ( F Fn A /\ G Fn A ) -> A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V )
61		eqid	\|- ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) = ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. )
62	61	fnmpo	\|- ( A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V -> ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) )
63	60 62	syl	\|- ( ( F Fn A /\ G Fn A ) -> ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) )
64	22	fneq1d	\|- ( ( F Fn A /\ G Fn A ) -> ( H Fn ( A X. A ) <-> ( x e. A , y e. A \|-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) ) )
65	63 64	mpbird	\|- ( ( F Fn A /\ G Fn A ) -> H Fn ( A X. A ) )
66	14	a1i	\|- ( ( ( F Fn A /\ G Fn A ) /\ a e. _V ) -> <. a , a >. e. _V )
67	66	ralrimiva	\|- ( ( F Fn A /\ G Fn A ) -> A. a e. _V <. a , a >. e. _V )
68	67 37	syl	\|- ( ( F Fn A /\ G Fn A ) -> ( a e. _V \|-> <. a , a >. ) Fn _V )
69	68 40 41	sylancl	\|- ( ( F Fn A /\ G Fn A ) -> ( ( a e. _V \|-> <. a , a >. ) \|` A ) Fn A )
70	69 46	sylibr	\|- ( ( F Fn A /\ G Fn A ) -> S Fn A )
71	45	rneqi	\|- ran S = ran ( ( a e. _V \|-> <. a , a >. ) \|` A )
72		mptima	\|- ( ( a e. _V \|-> <. a , a >. ) " A ) = ran ( a e. ( _V i^i A ) \|-> <. a , a >. )
73		df-ima	\|- ( ( a e. _V \|-> <. a , a >. ) " A ) = ran ( ( a e. _V \|-> <. a , a >. ) \|` A )
74		eqid	\|- ( a e. ( _V i^i A ) \|-> <. a , a >. ) = ( a e. ( _V i^i A ) \|-> <. a , a >. )
75	74	rnmpt	\|- ran ( a e. ( _V i^i A ) \|-> <. a , a >. ) = { p \| E. a e. ( _V i^i A ) p = <. a , a >. }
76	72 73 75	3eqtr3i	\|- ran ( ( a e. _V \|-> <. a , a >. ) \|` A ) = { p \| E. a e. ( _V i^i A ) p = <. a , a >. }
77	71 76	eqtri	\|- ran S = { p \| E. a e. ( _V i^i A ) p = <. a , a >. }
78		elinel2	\|- ( a e. ( _V i^i A ) -> a e. A )
79		simpl	\|- ( ( a e. A /\ p = <. a , a >. ) -> a e. A )
80	79 79	opelxpd	\|- ( ( a e. A /\ p = <. a , a >. ) -> <. a , a >. e. ( A X. A ) )
81		eleq1	\|- ( p = <. a , a >. -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) )
82	81	adantl	\|- ( ( a e. A /\ p = <. a , a >. ) -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) )
83	80 82	mpbird	\|- ( ( a e. A /\ p = <. a , a >. ) -> p e. ( A X. A ) )
84	83	ex	\|- ( a e. A -> ( p = <. a , a >. -> p e. ( A X. A ) ) )
85	78 84	syl	\|- ( a e. ( _V i^i A ) -> ( p = <. a , a >. -> p e. ( A X. A ) ) )
86	85	rexlimiv	\|- ( E. a e. ( _V i^i A ) p = <. a , a >. -> p e. ( A X. A ) )
87	86	abssi	\|- { p \| E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A )
88	87	a1i	\|- ( ( F Fn A /\ G Fn A ) -> { p \| E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A ) )
89	77 88	eqsstrid	\|- ( ( F Fn A /\ G Fn A ) -> ran S C_ ( A X. A ) )
90		fnco	\|- ( ( H Fn ( A X. A ) /\ S Fn A /\ ran S C_ ( A X. A ) ) -> ( H o. S ) Fn A )
91	65 70 89 90	syl3anc	\|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) Fn A )
92		opex	\|- <. ( F ` x ) , ( G ` x ) >. e. _V
93	92	a1i	\|- ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> <. ( F ` x ) , ( G ` x ) >. e. _V )
94	93	ralrimiva	\|- ( ( F Fn A /\ G Fn A ) -> A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V )
95	53	fnmpt	\|- ( A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V -> ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) Fn A )
96	94 95	syl	\|- ( ( F Fn A /\ G Fn A ) -> ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) Fn A )
97		eqfnfv	\|- ( ( ( H o. S ) Fn A /\ ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) Fn A ) -> ( ( H o. S ) = ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) )
98	91 96 97	syl2anc	\|- ( ( F Fn A /\ G Fn A ) -> ( ( H o. S ) = ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) )
99	57 98	mpbird	\|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( x e. A \|-> <. ( F ` x ) , ( G ` x ) >. ) )

Metamath Proof Explorer

Theorem fsplitfpar

Proof