caofdi

Description: Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypotheses	caofdi.1	$⊢ φ \to A \in V$
	caofdi.2	$⊢ φ \to F : A ⟶ K$
	caofdi.3	$⊢ φ \to G : A ⟶ S$
	caofdi.4	$⊢ φ \to H : A ⟶ S$
	caofdi.5	$⊢ (φ \land (x \in K \land y \in S \land z \in S)) \to x T (y R z) = (x T y) O (x T z)$
Assertion	caofdi	$⊢ φ \to F T_{f} (G R_{f} H) = (F T_{f} G) O_{f} (F T_{f} H)$

Proof

Step	Hyp	Ref	Expression
1		caofdi.1	$⊢ φ \to A \in V$
2		caofdi.2	$⊢ φ \to F : A ⟶ K$
3		caofdi.3	$⊢ φ \to G : A ⟶ S$
4		caofdi.4	$⊢ φ \to H : A ⟶ S$
5		caofdi.5	$⊢ (φ \land (x \in K \land y \in S \land z \in S)) \to x T (y R z) = (x T y) O (x T z)$
6	5	adantlr	$⊢ ((φ \land w \in A) \land (x \in K \land y \in S \land z \in S)) \to x T (y R z) = (x T y) O (x T z)$
7	2	ffvelrnda	$⊢ (φ \land w \in A) \to F (w) \in K$
8	3	ffvelrnda	$⊢ (φ \land w \in A) \to G (w) \in S$
9	4	ffvelrnda	$⊢ (φ \land w \in A) \to H (w) \in S$
10	6 7 8 9	caovdid	$⊢ (φ \land w \in A) \to F (w) T (G (w) R H (w)) = (F (w) T G (w)) O (F (w) T H (w))$
11	10	mpteq2dva	$⊢ φ \to (w \in A ⟼ F (w) T (G (w) R H (w))) = (w \in A ⟼ (F (w) T G (w)) O (F (w) T H (w)))$
12		ovexd	$⊢ (φ \land w \in A) \to G (w) R H (w) \in V$
13	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
14	3	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
15	4	feqmptd	$⊢ φ \to H = (w \in A ⟼ H (w))$
16	1 8 9 14 15	offval2	$⊢ φ \to G R_{f} H = (w \in A ⟼ G (w) R H (w))$
17	1 7 12 13 16	offval2	$⊢ φ \to F T_{f} (G R_{f} H) = (w \in A ⟼ F (w) T (G (w) R H (w)))$
18		ovexd	$⊢ (φ \land w \in A) \to F (w) T G (w) \in V$
19		ovexd	$⊢ (φ \land w \in A) \to F (w) T H (w) \in V$
20	1 7 8 13 14	offval2	$⊢ φ \to F T_{f} G = (w \in A ⟼ F (w) T G (w))$
21	1 7 9 13 15	offval2	$⊢ φ \to F T_{f} H = (w \in A ⟼ F (w) T H (w))$
22	1 18 19 20 21	offval2	$⊢ φ \to (F T_{f} G) O_{f} (F T_{f} H) = (w \in A ⟼ (F (w) T G (w)) O (F (w) T H (w)))$
23	11 17 22	3eqtr4d	$⊢ φ \to F T_{f} (G R_{f} H) = (F T_{f} G) O_{f} (F T_{f} H)$

Metamath Proof Explorer

Theorem caofdi

Proof