ofco2

Description: Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018)

		Ref	Expression
	Assertion	ofco2	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ H = (F \circ H) R_{f} (G \circ H)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to Fun H$
2		fvimacnvi	$⊢ (Fun H \land x \in H^{-1} [dom F \cap dom G]) \to H (x) \in (dom F \cap dom G)$
3	1 2	sylan	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in H^{-1} [dom F \cap dom G]) \to H (x) \in (dom F \cap dom G)$
4	1	funfnd	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to H Fn dom H$
5		dffn5	$⊢ H Fn dom H \leftrightarrow H = (x \in dom H ⟼ H (x))$
6	4 5	sylib	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to H = (x \in dom H ⟼ H (x))$
7	6	reseq1d	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to {H ↾}_{H^{-1} [dom F \cap dom G]} = {(x \in dom H ⟼ H (x)) ↾}_{H^{-1} [dom F \cap dom G]}$
8		cnvimass	$⊢ H^{-1} [dom F \cap dom G] \subseteq dom H$
9		resmpt	$⊢ H^{-1} [dom F \cap dom G] \subseteq dom H \to {(x \in dom H ⟼ H (x)) ↾}_{H^{-1} [dom F \cap dom G]} = (x \in H^{-1} [dom F \cap dom G] ⟼ H (x))$
10	8 9	ax-mp	$⊢ {(x \in dom H ⟼ H (x)) ↾}_{H^{-1} [dom F \cap dom G]} = (x \in H^{-1} [dom F \cap dom G] ⟼ H (x))$
11	7 10	eqtrdi	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to {H ↾}_{H^{-1} [dom F \cap dom G]} = (x \in H^{-1} [dom F \cap dom G] ⟼ H (x))$
12		offval3	$⊢ (F \in V \land G \in V) \to F R_{f} G = (y \in (dom F \cap dom G) ⟼ F (y) R G (y))$
13	12	adantr	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to F R_{f} G = (y \in (dom F \cap dom G) ⟼ F (y) R G (y))$
14		fveq2	$⊢ y = H (x) \to F (y) = F (H (x))$
15		fveq2	$⊢ y = H (x) \to G (y) = G (H (x))$
16	14 15	oveq12d	$⊢ y = H (x) \to F (y) R G (y) = F (H (x)) R G (H (x))$
17	3 11 13 16	fmptco	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ ({H ↾}_{H^{-1} [dom F \cap dom G]}) = (x \in H^{-1} [dom F \cap dom G] ⟼ F (H (x)) R G (H (x)))$
18		ovex	$⊢ F (x) R G (x) \in V$
19	18	rgenw	$⊢ \forall x \in (dom F \cap dom G) F (x) R G (x) \in V$
20		eqid	$⊢ (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
21	20	fnmpt	$⊢ \forall x \in (dom F \cap dom G) F (x) R G (x) \in V \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) Fn (dom F \cap dom G)$
22	19 21	mp1i	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) Fn (dom F \cap dom G)$
23		offval3	$⊢ (F \in V \land G \in V) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
24	23	adantr	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
25	24	fneq1d	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to ((F R_{f} G) Fn (dom F \cap dom G) \leftrightarrow (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) Fn (dom F \cap dom G))$
26	22 25	mpbird	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) Fn (dom F \cap dom G)$
27	26	fndmd	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to dom (F R_{f} G) = dom F \cap dom G$
28		eqimss	$⊢ dom (F R_{f} G) = dom F \cap dom G \to dom (F R_{f} G) \subseteq dom F \cap dom G$
29		cores2	$⊢ dom (F R_{f} G) \subseteq dom F \cap dom G \to (F R_{f} G) \circ {({H^{-1} ↾}_{(dom F \cap dom G)})}^{-1} = (F R_{f} G) \circ H$
30	27 28 29	3syl	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ {({H^{-1} ↾}_{(dom F \cap dom G)})}^{-1} = (F R_{f} G) \circ H$
31		funcnvres2	$⊢ Fun H \to {({H^{-1} ↾}_{(dom F \cap dom G)})}^{-1} = {H ↾}_{H^{-1} [dom F \cap dom G]}$
32	1 31	syl	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to {({H^{-1} ↾}_{(dom F \cap dom G)})}^{-1} = {H ↾}_{H^{-1} [dom F \cap dom G]}$
33	32	coeq2d	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ {({H^{-1} ↾}_{(dom F \cap dom G)})}^{-1} = (F R_{f} G) \circ ({H ↾}_{H^{-1} [dom F \cap dom G]})$
34	30 33	eqtr3d	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ H = (F R_{f} G) \circ ({H ↾}_{H^{-1} [dom F \cap dom G]})$
35		simpr2	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to F \circ H \in V$
36		simpr3	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to G \circ H \in V$
37		offval3	$⊢ (F \circ H \in V \land G \circ H \in V) \to (F \circ H) R_{f} (G \circ H) = (x \in (dom (F \circ H) \cap dom (G \circ H)) ⟼ (F \circ H) (x) R (G \circ H) (x))$
38	35 36 37	syl2anc	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F \circ H) R_{f} (G \circ H) = (x \in (dom (F \circ H) \cap dom (G \circ H)) ⟼ (F \circ H) (x) R (G \circ H) (x))$
39		dmco	$⊢ dom (F \circ H) = H^{-1} [dom F]$
40		dmco	$⊢ dom (G \circ H) = H^{-1} [dom G]$
41	39 40	ineq12i	$⊢ dom (F \circ H) \cap dom (G \circ H) = H^{-1} [dom F] \cap H^{-1} [dom G]$
42		inpreima	$⊢ Fun H \to H^{-1} [dom F \cap dom G] = H^{-1} [dom F] \cap H^{-1} [dom G]$
43	1 42	syl	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to H^{-1} [dom F \cap dom G] = H^{-1} [dom F] \cap H^{-1} [dom G]$
44	41 43	eqtr4id	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to dom (F \circ H) \cap dom (G \circ H) = H^{-1} [dom F \cap dom G]$
45		simplr1	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to Fun H$
46		inss2	$⊢ dom (F \circ H) \cap dom (G \circ H) \subseteq dom (G \circ H)$
47		dmcoss	$⊢ dom (G \circ H) \subseteq dom H$
48	46 47	sstri	$⊢ dom (F \circ H) \cap dom (G \circ H) \subseteq dom H$
49	48	a1i	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to dom (F \circ H) \cap dom (G \circ H) \subseteq dom H$
50	49	sselda	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to x \in dom H$
51		fvco	$⊢ (Fun H \land x \in dom H) \to (F \circ H) (x) = F (H (x))$
52	45 50 51	syl2anc	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to (F \circ H) (x) = F (H (x))$
53		inss1	$⊢ dom (F \circ H) \cap dom (G \circ H) \subseteq dom (F \circ H)$
54		dmcoss	$⊢ dom (F \circ H) \subseteq dom H$
55	53 54	sstri	$⊢ dom (F \circ H) \cap dom (G \circ H) \subseteq dom H$
56	55	a1i	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to dom (F \circ H) \cap dom (G \circ H) \subseteq dom H$
57	56	sselda	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to x \in dom H$
58		fvco	$⊢ (Fun H \land x \in dom H) \to (G \circ H) (x) = G (H (x))$
59	45 57 58	syl2anc	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to (G \circ H) (x) = G (H (x))$
60	52 59	oveq12d	$⊢ (((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \land x \in (dom (F \circ H) \cap dom (G \circ H))) \to (F \circ H) (x) R (G \circ H) (x) = F (H (x)) R G (H (x))$
61	44 60	mpteq12dva	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (x \in (dom (F \circ H) \cap dom (G \circ H)) ⟼ (F \circ H) (x) R (G \circ H) (x)) = (x \in H^{-1} [dom F \cap dom G] ⟼ F (H (x)) R G (H (x)))$
62	38 61	eqtrd	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F \circ H) R_{f} (G \circ H) = (x \in H^{-1} [dom F \cap dom G] ⟼ F (H (x)) R G (H (x)))$
63	17 34 62	3eqtr4d	$⊢ ((F \in V \land G \in V) \land (Fun H \land F \circ H \in V \land G \circ H \in V)) \to (F R_{f} G) \circ H = (F \circ H) R_{f} (G \circ H)$

Metamath Proof Explorer

Theorem ofco2

Proof