Theorem oprab2co

Description: Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by David Abernethy, 23-Apr-2013)

	Ref	Expression
Hypotheses	oprab2co.1	|- ( ( x e. A /\ y e. B ) -> C e. R )
	oprab2co.2	|- ( ( x e. A /\ y e. B ) -> D e. S )
	oprab2co.3	|- F = ( x e. A , y e. B |-> <. C , D >. )
	oprab2co.4	|- G = ( x e. A , y e. B |-> ( C M D ) )
Assertion	oprab2co	|- ( M Fn ( R X. S ) -> G = ( M o. F ) )

Proof

Step	Hyp	Ref	Expression
1		oprab2co.1	|- ( ( x e. A /\ y e. B ) -> C e. R )
2		oprab2co.2	|- ( ( x e. A /\ y e. B ) -> D e. S )
3		oprab2co.3	|- F = ( x e. A , y e. B |-> <. C , D >. )
4		oprab2co.4	|- G = ( x e. A , y e. B |-> ( C M D ) )
5	1 2	opelxpd	|- ( ( x e. A /\ y e. B ) -> <. C , D >. e. ( R X. S ) )
6		df-ov	|- ( C M D ) = ( M ` <. C , D >. )
7	6	a1i	|- ( ( x e. A /\ y e. B ) -> ( C M D ) = ( M ` <. C , D >. ) )
8	7	mpoeq3ia	|- ( x e. A , y e. B |-> ( C M D ) ) = ( x e. A , y e. B |-> ( M ` <. C , D >. ) )
9	4 8	eqtri	|- G = ( x e. A , y e. B |-> ( M ` <. C , D >. ) )
10	5 3 9	oprabco	|- ( M Fn ( R X. S ) -> G = ( M o. F ) )