fvcofneq

Description: The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019)

		Ref	Expression
	Assertion	fvcofneq	$⊢ (G Fn A \land K Fn B) \to ((X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to (F \circ G) (X) = (H \circ K) (X))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (G Fn A \land K Fn B) \to G Fn A$
2		elinel1	$⊢ X \in (A \cap B) \to X \in A$
3	2	3ad2ant1	$⊢ (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to X \in A$
4		fvco2	$⊢ (G Fn A \land X \in A) \to (F \circ G) (X) = F (G (X))$
5	1 3 4	syl2an	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to (F \circ G) (X) = F (G (X))$
6		simpr	$⊢ (G Fn A \land K Fn B) \to K Fn B$
7		elinel2	$⊢ X \in (A \cap B) \to X \in B$
8	7	3ad2ant1	$⊢ (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to X \in B$
9		fvco2	$⊢ (K Fn B \land X \in B) \to (H \circ K) (X) = H (K (X))$
10	6 8 9	syl2an	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to (H \circ K) (X) = H (K (X))$
11		fveq2	$⊢ K (X) = G (X) \to H (K (X)) = H (G (X))$
12	11	eqcoms	$⊢ G (X) = K (X) \to H (K (X)) = H (G (X))$
13	12	3ad2ant2	$⊢ (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to H (K (X)) = H (G (X))$
14	13	adantl	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to H (K (X)) = H (G (X))$
15		id	$⊢ G Fn A \to G Fn A$
16		fnfvelrn	$⊢ (G Fn A \land X \in A) \to G (X) \in ran G$
17	15 2 16	syl2anr	$⊢ (X \in (A \cap B) \land G Fn A) \to G (X) \in ran G$
18	17	ex	$⊢ X \in (A \cap B) \to (G Fn A \to G (X) \in ran G)$
19		id	$⊢ K Fn B \to K Fn B$
20		fnfvelrn	$⊢ (K Fn B \land X \in B) \to K (X) \in ran K$
21	19 7 20	syl2anr	$⊢ (X \in (A \cap B) \land K Fn B) \to K (X) \in ran K$
22	21	ex	$⊢ X \in (A \cap B) \to (K Fn B \to K (X) \in ran K)$
23	18 22	anim12d	$⊢ X \in (A \cap B) \to ((G Fn A \land K Fn B) \to (G (X) \in ran G \land K (X) \in ran K))$
24		eleq1	$⊢ K (X) = G (X) \to (K (X) \in ran K \leftrightarrow G (X) \in ran K)$
25	24	eqcoms	$⊢ G (X) = K (X) \to (K (X) \in ran K \leftrightarrow G (X) \in ran K)$
26	25	anbi2d	$⊢ G (X) = K (X) \to ((G (X) \in ran G \land K (X) \in ran K) \leftrightarrow (G (X) \in ran G \land G (X) \in ran K))$
27		elin	$⊢ G (X) \in (ran G \cap ran K) \leftrightarrow (G (X) \in ran G \land G (X) \in ran K)$
28	27	biimpri	$⊢ (G (X) \in ran G \land G (X) \in ran K) \to G (X) \in (ran G \cap ran K)$
29	26 28	syl6bi	$⊢ G (X) = K (X) \to ((G (X) \in ran G \land K (X) \in ran K) \to G (X) \in (ran G \cap ran K))$
30	23 29	sylan9	$⊢ (X \in (A \cap B) \land G (X) = K (X)) \to ((G Fn A \land K Fn B) \to G (X) \in (ran G \cap ran K))$
31		fveq2	$⊢ x = G (X) \to F (x) = F (G (X))$
32		fveq2	$⊢ x = G (X) \to H (x) = H (G (X))$
33	31 32	eqeq12d	$⊢ x = G (X) \to (F (x) = H (x) \leftrightarrow F (G (X)) = H (G (X)))$
34	33	rspcva	$⊢ (G (X) \in (ran G \cap ran K) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to F (G (X)) = H (G (X))$
35	34	eqcomd	$⊢ (G (X) \in (ran G \cap ran K) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to H (G (X)) = F (G (X))$
36	35	ex	$⊢ G (X) \in (ran G \cap ran K) \to (\forall x \in (ran G \cap ran K) F (x) = H (x) \to H (G (X)) = F (G (X)))$
37	30 36	syl6	$⊢ (X \in (A \cap B) \land G (X) = K (X)) \to ((G Fn A \land K Fn B) \to (\forall x \in (ran G \cap ran K) F (x) = H (x) \to H (G (X)) = F (G (X))))$
38	37	com23	$⊢ (X \in (A \cap B) \land G (X) = K (X)) \to (\forall x \in (ran G \cap ran K) F (x) = H (x) \to ((G Fn A \land K Fn B) \to H (G (X)) = F (G (X))))$
39	38	3impia	$⊢ (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to ((G Fn A \land K Fn B) \to H (G (X)) = F (G (X)))$
40	39	impcom	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to H (G (X)) = F (G (X))$
41	10 14 40	3eqtrrd	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to F (G (X)) = (H \circ K) (X)$
42	5 41	eqtrd	$⊢ ((G Fn A \land K Fn B) \land (X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x))) \to (F \circ G) (X) = (H \circ K) (X)$
43	42	ex	$⊢ (G Fn A \land K Fn B) \to ((X \in (A \cap B) \land G (X) = K (X) \land \forall x \in (ran G \cap ran K) F (x) = H (x)) \to (F \circ G) (X) = (H \circ K) (X))$

Metamath Proof Explorer

Theorem fvcofneq

Proof