Metamath Proof Explorer

Theorem oftpos

Description: The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018)

		Ref	Expression
	Assertion	oftpos	$⊢ (F \in V \land G \in W) \to tpos (F R_{f} G) = tpos F R_{f} tpos G$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ F \in V \to F \in V$
2	1	adantr	$⊢ (F \in V \land G \in W) \to F \in V$
3		elex	$⊢ G \in W \to G \in V$
4	3	adantl	$⊢ (F \in V \land G \in W) \to G \in V$
5		funmpt	$⊢ Fun (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
6	5	a1i	$⊢ (F \in V \land G \in W) \to Fun (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
7		dftpos4	$⊢ tpos F = F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
8		tposexg	$⊢ F \in V \to tpos F \in V$
9	8	adantr	$⊢ (F \in V \land G \in W) \to tpos F \in V$
10	7 9	eqeltrrid	$⊢ (F \in V \land G \in W) \to F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \in V$
11		dftpos4	$⊢ tpos G = G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
12		tposexg	$⊢ G \in W \to tpos G \in V$
13	12	adantl	$⊢ (F \in V \land G \in W) \to tpos G \in V$
14	11 13	eqeltrrid	$⊢ (F \in V \land G \in W) \to G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \in V$
15		ofco2	$⊢ ((F \in V \land G \in V) \land (Fun (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \land F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \in V \land G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \in V)) \to (F R_{f} G) \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) R_{f} (G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
16	2 4 6 10 14 15	syl23anc	$⊢ (F \in V \land G \in W) \to (F R_{f} G) \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) R_{f} (G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
17		dftpos4	$⊢ tpos (F R_{f} G) = (F R_{f} G) \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
18	7 11	oveq12i	$⊢ tpos F R_{f} tpos G = (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) R_{f} (G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
19	16 17 18	3eqtr4g	$⊢ (F \in V \land G \in W) \to tpos (F R_{f} G) = tpos F R_{f} tpos G$