caofdir

Description: Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-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$
	caofdir.5	$⊢ (φ \land (x \in S \land y \in S \land z \in K)) \to (x R y) T z = (x T z) O (y T z)$
Assertion	caofdir	$⊢ φ \to (G R_{f} H) T_{f} F = (G T_{f} F) O_{f} (H T_{f} F)$

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		caofdir.5	$⊢ (φ \land (x \in S \land y \in S \land z \in K)) \to (x R y) T z = (x T z) O (y T z)$
6	5	adantlr	$⊢ ((φ \land w \in A) \land (x \in S \land y \in S \land z \in K)) \to (x R y) T z = (x T z) O (y T z)$
7	3	ffvelrnda	$⊢ (φ \land w \in A) \to G (w) \in S$
8	4	ffvelrnda	$⊢ (φ \land w \in A) \to H (w) \in S$
9	2	ffvelrnda	$⊢ (φ \land w \in A) \to F (w) \in K$
10	6 7 8 9	caovdird	$⊢ (φ \land w \in A) \to (G (w) R H (w)) T F (w) = (G (w) T F (w)) O (H (w) T F (w))$
11	10	mpteq2dva	$⊢ φ \to (w \in A ⟼ (G (w) R H (w)) T F (w)) = (w \in A ⟼ (G (w) T F (w)) O (H (w) T F (w)))$
12		ovexd	$⊢ (φ \land w \in A) \to G (w) R H (w) \in V$
13	3	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
14	4	feqmptd	$⊢ φ \to H = (w \in A ⟼ H (w))$
15	1 7 8 13 14	offval2	$⊢ φ \to G R_{f} H = (w \in A ⟼ G (w) R H (w))$
16	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
17	1 12 9 15 16	offval2	$⊢ φ \to (G R_{f} H) T_{f} F = (w \in A ⟼ (G (w) R H (w)) T F (w))$
18		ovexd	$⊢ (φ \land w \in A) \to G (w) T F (w) \in V$
19		ovexd	$⊢ (φ \land w \in A) \to H (w) T F (w) \in V$
20	1 7 9 13 16	offval2	$⊢ φ \to G T_{f} F = (w \in A ⟼ G (w) T F (w))$
21	1 8 9 14 16	offval2	$⊢ φ \to H T_{f} F = (w \in A ⟼ H (w) T F (w))$
22	1 18 19 20 21	offval2	$⊢ φ \to (G T_{f} F) O_{f} (H T_{f} F) = (w \in A ⟼ (G (w) T F (w)) O (H (w) T F (w)))$
23	11 17 22	3eqtr4d	$⊢ φ \to (G R_{f} H) T_{f} F = (G T_{f} F) O_{f} (H T_{f} F)$

Metamath Proof Explorer

Theorem caofdir

Proof