ofmul12

Description: Function analogue of mul12 . (Contributed by Steve Rodriguez, 13-Nov-2015)

		Ref	Expression
	Assertion	ofmul12	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to F \times_{f} (G \times_{f} H) = G \times_{f} (F \times_{f} H)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to A \in V$
2		simplr	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to F : A ⟶ ℂ$
3	2	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to F Fn A$
4		simprl	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to G : A ⟶ ℂ$
5	4	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to G Fn A$
6		simprr	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to H : A ⟶ ℂ$
7	6	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to H Fn A$
8		inidm	$⊢ A \cap A = A$
9	5 7 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to (G \times_{f} H) Fn A$
10	3 7 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to (F \times_{f} H) Fn A$
11	5 10 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to (G \times_{f} (F \times_{f} H)) Fn A$
12		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to F (x) = F (x)$
13		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to G (x) = G (x)$
14		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to H (x) = H (x)$
15	5 7 1 1 8 13 14	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to (G \times_{f} H) (x) = G (x) H (x)$
16	2	ffvelcdmda	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to F (x) \in ℂ$
17	4	ffvelcdmda	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to G (x) \in ℂ$
18	6	ffvelcdmda	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to H (x) \in ℂ$
19	16 17 18	mul12d	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to F (x) G (x) H (x) = G (x) F (x) H (x)$
20	3 7 1 1 8 12 14	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to (F \times_{f} H) (x) = F (x) H (x)$
21	5 10 1 1 8 13 20	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to (G \times_{f} (F \times_{f} H)) (x) = G (x) F (x) H (x)$
22	19 21	eqtr4d	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \land x \in A) \to F (x) G (x) H (x) = (G \times_{f} (F \times_{f} H)) (x)$
23	1 3 9 11 12 15 22	offveq	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ \land H : A ⟶ ℂ)) \to F \times_{f} (G \times_{f} H) = G \times_{f} (F \times_{f} H)$

Metamath Proof Explorer

Theorem ofmul12

Proof