msubco

Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016)

		Ref	Expression
	Hypothesis	msubco.s	$⊢ S = mSubst (T)$
	Assertion	msubco	$⊢ (F \in ran S \land G \in ran S) \to F \circ G \in ran S$

Proof

Step	Hyp	Ref	Expression
1		msubco.s	$⊢ S = mSubst (T)$
2		eqid	$⊢ mEx (T) = mEx (T)$
3		eqid	$⊢ mRSubst (T) = mRSubst (T)$
4	2 3 1	elmsubrn	$⊢ ran S = ran (f \in ran mRSubst (T) ⟼ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩))$
5	4	eleq2i	$⊢ F \in ran S \leftrightarrow F \in ran (f \in ran mRSubst (T) ⟼ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩))$
6		eqid	$⊢ (f \in ran mRSubst (T) ⟼ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩)) = (f \in ran mRSubst (T) ⟼ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩))$
7		fvex	$⊢ mEx (T) \in V$
8	7	mptex	$⊢ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \in V$
9	6 8	elrnmpti	$⊢ F \in ran (f \in ran mRSubst (T) ⟼ (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩)) \leftrightarrow \exists f \in ran mRSubst (T) F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩)$
10	5 9	bitri	$⊢ F \in ran S \leftrightarrow \exists f \in ran mRSubst (T) F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩)$
11	2 3 1	elmsubrn	$⊢ ran S = ran (g \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩))$
12	11	eleq2i	$⊢ G \in ran S \leftrightarrow G \in ran (g \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩))$
13		eqid	$⊢ (g \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) = (g \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩))$
14	7	mptex	$⊢ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) \in V$
15	13 14	elrnmpti	$⊢ G \in ran (g \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \leftrightarrow \exists g \in ran mRSubst (T) G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)$
16	12 15	bitri	$⊢ G \in ran S \leftrightarrow \exists g \in ran mRSubst (T) G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)$
17		reeanv	$⊢ \exists f \in ran mRSubst (T) \exists g \in ran mRSubst (T) (F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \leftrightarrow (\exists f \in ran mRSubst (T) F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land \exists g \in ran mRSubst (T) G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩))$
18		simpr	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to y \in mEx (T)$
19		eqid	$⊢ mTC (T) = mTC (T)$
20		eqid	$⊢ mREx (T) = mREx (T)$
21	19 2 20	mexval	$⊢ mEx (T) = mTC (T) \times mREx (T)$
22	18 21	eleqtrdi	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to y \in (mTC (T) \times mREx (T))$
23		xp1st	$⊢ y \in (mTC (T) \times mREx (T)) \to 1^{st} (y) \in mTC (T)$
24	22 23	syl	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to 1^{st} (y) \in mTC (T)$
25	3 20	mrsubf	$⊢ g \in ran mRSubst (T) \to g : mREx (T) ⟶ mREx (T)$
26	25	ad2antlr	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to g : mREx (T) ⟶ mREx (T)$
27		xp2nd	$⊢ y \in (mTC (T) \times mREx (T)) \to 2^{nd} (y) \in mREx (T)$
28	22 27	syl	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to 2^{nd} (y) \in mREx (T)$
29	26 28	ffvelcdmd	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to g (2^{nd} (y)) \in mREx (T)$
30		opelxpi	$⊢ (1^{st} (y) \in mTC (T) \land g (2^{nd} (y)) \in mREx (T)) \to ⟨1^{st} (y), g (2^{nd} (y))⟩ \in (mTC (T) \times mREx (T))$
31	24 29 30	syl2anc	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to ⟨1^{st} (y), g (2^{nd} (y))⟩ \in (mTC (T) \times mREx (T))$
32	31 21	eleqtrrdi	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to ⟨1^{st} (y), g (2^{nd} (y))⟩ \in mEx (T)$
33		eqidd	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)$
34		eqidd	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩)$
35		fvex	$⊢ 1^{st} (y) \in V$
36		fvex	$⊢ g (2^{nd} (y)) \in V$
37	35 36	op1std	$⊢ x = ⟨1^{st} (y), g (2^{nd} (y))⟩ \to 1^{st} (x) = 1^{st} (y)$
38	35 36	op2ndd	$⊢ x = ⟨1^{st} (y), g (2^{nd} (y))⟩ \to 2^{nd} (x) = g (2^{nd} (y))$
39	38	fveq2d	$⊢ x = ⟨1^{st} (y), g (2^{nd} (y))⟩ \to f (2^{nd} (x)) = f (g (2^{nd} (y)))$
40	37 39	opeq12d	$⊢ x = ⟨1^{st} (y), g (2^{nd} (y))⟩ \to ⟨1^{st} (x), f (2^{nd} (x))⟩ = ⟨1^{st} (y), f (g (2^{nd} (y)))⟩$
41	32 33 34 40	fmptco	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) = (y \in mEx (T) ⟼ ⟨1^{st} (y), f (g (2^{nd} (y)))⟩)$
42		fvco3	$⊢ (g : mREx (T) ⟶ mREx (T) \land 2^{nd} (y) \in mREx (T)) \to (f \circ g) (2^{nd} (y)) = f (g (2^{nd} (y)))$
43	26 28 42	syl2anc	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to (f \circ g) (2^{nd} (y)) = f (g (2^{nd} (y)))$
44	43	opeq2d	$⊢ ((f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \land y \in mEx (T)) \to ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩ = ⟨1^{st} (y), f (g (2^{nd} (y)))⟩$
45	44	mpteq2dva	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) = (y \in mEx (T) ⟼ ⟨1^{st} (y), f (g (2^{nd} (y)))⟩)$
46	41 45	eqtr4d	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) = (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩)$
47	3	mrsubco	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to f \circ g \in ran mRSubst (T)$
48	7	mptex	$⊢ (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) \in V$
49		eqid	$⊢ (h \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩)) = (h \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩))$
50		fveq1	$⊢ h = f \circ g \to h (2^{nd} (y)) = (f \circ g) (2^{nd} (y))$
51	50	opeq2d	$⊢ h = f \circ g \to ⟨1^{st} (y), h (2^{nd} (y))⟩ = ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩$
52	51	mpteq2dv	$⊢ h = f \circ g \to (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩) = (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩)$
53	49 52	elrnmpt1s	$⊢ (f \circ g \in ran mRSubst (T) \land (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) \in V) \to (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) \in ran (h \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩))$
54	47 48 53	sylancl	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) \in ran (h \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩))$
55	2 3 1	elmsubrn	$⊢ ran S = ran (h \in ran mRSubst (T) ⟼ (y \in mEx (T) ⟼ ⟨1^{st} (y), h (2^{nd} (y))⟩))$
56	54 55	eleqtrrdi	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (y \in mEx (T) ⟼ ⟨1^{st} (y), (f \circ g) (2^{nd} (y))⟩) \in ran S$
57	46 56	eqeltrd	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) \in ran S$
58		coeq1	$⊢ F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \to F \circ G = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ G$
59		coeq2	$⊢ G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) \to (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ G = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)$
60	58 59	sylan9eq	$⊢ (F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \to F \circ G = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)$
61	60	eleq1d	$⊢ (F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \to (F \circ G \in ran S \leftrightarrow (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \circ (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩) \in ran S)$
62	57 61	syl5ibrcom	$⊢ (f \in ran mRSubst (T) \land g \in ran mRSubst (T)) \to ((F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \to F \circ G \in ran S)$
63	62	rexlimivv	$⊢ \exists f \in ran mRSubst (T) \exists g \in ran mRSubst (T) (F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \to F \circ G \in ran S$
64	17 63	sylbir	$⊢ (\exists f \in ran mRSubst (T) F = (x \in mEx (T) ⟼ ⟨1^{st} (x), f (2^{nd} (x))⟩) \land \exists g \in ran mRSubst (T) G = (y \in mEx (T) ⟼ ⟨1^{st} (y), g (2^{nd} (y))⟩)) \to F \circ G \in ran S$
65	10 16 64	syl2anb	$⊢ (F \in ran S \land G \in ran S) \to F \circ G \in ran S$

Metamath Proof Explorer

Theorem msubco

Proof