caofass

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

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

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofcom.3	$⊢ φ \to G : A ⟶ S$
4		caofass.4	$⊢ φ \to H : A ⟶ S$
5		caofass.5	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y) T z = x O (y P z)$
6	5	ralrimivvva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S (x R y) T z = x O (y P z)$
7	6	adantr	$⊢ (φ \land w \in A) \to \forall x \in S \forall y \in S \forall z \in S (x R y) T z = x O (y P z)$
8	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
9	3	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
10	4	ffvelcdmda	$⊢ (φ \land w \in A) \to H (w) \in S$
11		oveq1	$⊢ x = F (w) \to x R y = F (w) R y$
12	11	oveq1d	$⊢ x = F (w) \to (x R y) T z = (F (w) R y) T z$
13		oveq1	$⊢ x = F (w) \to x O (y P z) = F (w) O (y P z)$
14	12 13	eqeq12d	$⊢ x = F (w) \to ((x R y) T z = x O (y P z) \leftrightarrow (F (w) R y) T z = F (w) O (y P z))$
15		oveq2	$⊢ y = G (w) \to F (w) R y = F (w) R G (w)$
16	15	oveq1d	$⊢ y = G (w) \to (F (w) R y) T z = (F (w) R G (w)) T z$
17		oveq1	$⊢ y = G (w) \to y P z = G (w) P z$
18	17	oveq2d	$⊢ y = G (w) \to F (w) O (y P z) = F (w) O (G (w) P z)$
19	16 18	eqeq12d	$⊢ y = G (w) \to ((F (w) R y) T z = F (w) O (y P z) \leftrightarrow (F (w) R G (w)) T z = F (w) O (G (w) P z))$
20		oveq2	$⊢ z = H (w) \to (F (w) R G (w)) T z = (F (w) R G (w)) T H (w)$
21		oveq2	$⊢ z = H (w) \to G (w) P z = G (w) P H (w)$
22	21	oveq2d	$⊢ z = H (w) \to F (w) O (G (w) P z) = F (w) O (G (w) P H (w))$
23	20 22	eqeq12d	$⊢ z = H (w) \to ((F (w) R G (w)) T z = F (w) O (G (w) P z) \leftrightarrow (F (w) R G (w)) T H (w) = F (w) O (G (w) P H (w)))$
24	14 19 23	rspc3v	$⊢ (F (w) \in S \land G (w) \in S \land H (w) \in S) \to (\forall x \in S \forall y \in S \forall z \in S (x R y) T z = x O (y P z) \to (F (w) R G (w)) T H (w) = F (w) O (G (w) P H (w)))$
25	8 9 10 24	syl3anc	$⊢ (φ \land w \in A) \to (\forall x \in S \forall y \in S \forall z \in S (x R y) T z = x O (y P z) \to (F (w) R G (w)) T H (w) = F (w) O (G (w) P H (w)))$
26	7 25	mpd	$⊢ (φ \land w \in A) \to (F (w) R G (w)) T H (w) = F (w) O (G (w) P H (w))$
27	26	mpteq2dva	$⊢ φ \to (w \in A ⟼ (F (w) R G (w)) T H (w)) = (w \in A ⟼ F (w) O (G (w) P H (w)))$
28		ovexd	$⊢ (φ \land w \in A) \to F (w) R G (w) \in V$
29	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
30	3	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
31	1 8 9 29 30	offval2	$⊢ φ \to F R_{f} G = (w \in A ⟼ F (w) R G (w))$
32	4	feqmptd	$⊢ φ \to H = (w \in A ⟼ H (w))$
33	1 28 10 31 32	offval2	$⊢ φ \to (F R_{f} G) T_{f} H = (w \in A ⟼ (F (w) R G (w)) T H (w))$
34		ovexd	$⊢ (φ \land w \in A) \to G (w) P H (w) \in V$
35	1 9 10 30 32	offval2	$⊢ φ \to G P_{f} H = (w \in A ⟼ G (w) P H (w))$
36	1 8 34 29 35	offval2	$⊢ φ \to F O_{f} (G P_{f} H) = (w \in A ⟼ F (w) O (G (w) P H (w)))$
37	27 33 36	3eqtr4d	$⊢ φ \to (F R_{f} G) T_{f} H = F O_{f} (G P_{f} H)$

Metamath Proof Explorer

Theorem caofass

Proof