mrsubco

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

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

Proof

Step	Hyp	Ref	Expression
1		mrsubco.s	$⊢ S = mRSubst (T)$
2		eqid	$⊢ mREx (T) = mREx (T)$
3	1 2	mrsubf	$⊢ F \in ran S \to F : mREx (T) ⟶ mREx (T)$
4	3	adantr	$⊢ (F \in ran S \land G \in ran S) \to F : mREx (T) ⟶ mREx (T)$
5	1 2	mrsubf	$⊢ G \in ran S \to G : mREx (T) ⟶ mREx (T)$
6	5	adantl	$⊢ (F \in ran S \land G \in ran S) \to G : mREx (T) ⟶ mREx (T)$
7		fco	$⊢ (F : mREx (T) ⟶ mREx (T) \land G : mREx (T) ⟶ mREx (T)) \to (F \circ G) : mREx (T) ⟶ mREx (T)$
8	4 6 7	syl2anc	$⊢ (F \in ran S \land G \in ran S) \to (F \circ G) : mREx (T) ⟶ mREx (T)$
9	6	adantr	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to G : mREx (T) ⟶ mREx (T)$
10		eldifi	$⊢ c \in (mCN (T) ∖ mVR (T)) \to c \in mCN (T)$
11		elun1	$⊢ c \in mCN (T) \to c \in (mCN (T) \cup mVR (T))$
12	10 11	syl	$⊢ c \in (mCN (T) ∖ mVR (T)) \to c \in (mCN (T) \cup mVR (T))$
13	12	adantl	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to c \in (mCN (T) \cup mVR (T))$
14	13	s1cld	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to ⟨“ c ”⟩ \in Word (mCN (T) \cup mVR (T))$
15		n0i	$⊢ F \in ran S \to \neg ran S = \emptyset$
16	1	rnfvprc	$⊢ \neg T \in V \to ran S = \emptyset$
17	15 16	nsyl2	$⊢ F \in ran S \to T \in V$
18	17	adantr	$⊢ (F \in ran S \land G \in ran S) \to T \in V$
19	18	adantr	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to T \in V$
20		eqid	$⊢ mCN (T) = mCN (T)$
21		eqid	$⊢ mVR (T) = mVR (T)$
22	20 21 2	mrexval	$⊢ T \in V \to mREx (T) = Word (mCN (T) \cup mVR (T))$
23	19 22	syl	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to mREx (T) = Word (mCN (T) \cup mVR (T))$
24	14 23	eleqtrrd	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to ⟨“ c ”⟩ \in mREx (T)$
25		fvco3	$⊢ (G : mREx (T) ⟶ mREx (T) \land ⟨“ c ”⟩ \in mREx (T)) \to (F \circ G) (⟨“ c ”⟩) = F (G (⟨“ c ”⟩))$
26	9 24 25	syl2anc	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to (F \circ G) (⟨“ c ”⟩) = F (G (⟨“ c ”⟩))$
27	1 2 21 20	mrsubcn	$⊢ (G \in ran S \land c \in (mCN (T) ∖ mVR (T))) \to G (⟨“ c ”⟩) = ⟨“ c ”⟩$
28	27	adantll	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to G (⟨“ c ”⟩) = ⟨“ c ”⟩$
29	28	fveq2d	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to F (G (⟨“ c ”⟩)) = F (⟨“ c ”⟩)$
30	1 2 21 20	mrsubcn	$⊢ (F \in ran S \land c \in (mCN (T) ∖ mVR (T))) \to F (⟨“ c ”⟩) = ⟨“ c ”⟩$
31	30	adantlr	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to F (⟨“ c ”⟩) = ⟨“ c ”⟩$
32	26 29 31	3eqtrd	$⊢ ((F \in ran S \land G \in ran S) \land c \in (mCN (T) ∖ mVR (T))) \to (F \circ G) (⟨“ c ”⟩) = ⟨“ c ”⟩$
33	32	ralrimiva	$⊢ (F \in ran S \land G \in ran S) \to \forall c \in (mCN (T) ∖ mVR (T)) (F \circ G) (⟨“ c ”⟩) = ⟨“ c ”⟩$
34	1 2	mrsubccat	$⊢ (G \in ran S \land x \in mREx (T) \land y \in mREx (T)) \to G (x ++ y) = G (x) ++ G (y)$
35	34	3expb	$⊢ (G \in ran S \land (x \in mREx (T) \land y \in mREx (T))) \to G (x ++ y) = G (x) ++ G (y)$
36	35	adantll	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to G (x ++ y) = G (x) ++ G (y)$
37	36	fveq2d	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to F (G (x ++ y)) = F (G (x) ++ G (y))$
38		simpll	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to F \in ran S$
39	6	adantr	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to G : mREx (T) ⟶ mREx (T)$
40		simprl	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to x \in mREx (T)$
41	39 40	ffvelcdmd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to G (x) \in mREx (T)$
42		simprr	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to y \in mREx (T)$
43	39 42	ffvelcdmd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to G (y) \in mREx (T)$
44	1 2	mrsubccat	$⊢ (F \in ran S \land G (x) \in mREx (T) \land G (y) \in mREx (T)) \to F (G (x) ++ G (y)) = F (G (x)) ++ F (G (y))$
45	38 41 43 44	syl3anc	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to F (G (x) ++ G (y)) = F (G (x)) ++ F (G (y))$
46	37 45	eqtrd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to F (G (x ++ y)) = F (G (x)) ++ F (G (y))$
47	18 22	syl	$⊢ (F \in ran S \land G \in ran S) \to mREx (T) = Word (mCN (T) \cup mVR (T))$
48	47	adantr	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to mREx (T) = Word (mCN (T) \cup mVR (T))$
49	40 48	eleqtrd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to x \in Word (mCN (T) \cup mVR (T))$
50	42 48	eleqtrd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to y \in Word (mCN (T) \cup mVR (T))$
51		ccatcl	$⊢ (x \in Word (mCN (T) \cup mVR (T)) \land y \in Word (mCN (T) \cup mVR (T))) \to x ++ y \in Word (mCN (T) \cup mVR (T))$
52	49 50 51	syl2anc	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to x ++ y \in Word (mCN (T) \cup mVR (T))$
53	52 48	eleqtrrd	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to x ++ y \in mREx (T)$
54		fvco3	$⊢ (G : mREx (T) ⟶ mREx (T) \land x ++ y \in mREx (T)) \to (F \circ G) (x ++ y) = F (G (x ++ y))$
55	39 53 54	syl2anc	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to (F \circ G) (x ++ y) = F (G (x ++ y))$
56		fvco3	$⊢ (G : mREx (T) ⟶ mREx (T) \land x \in mREx (T)) \to (F \circ G) (x) = F (G (x))$
57	39 40 56	syl2anc	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to (F \circ G) (x) = F (G (x))$
58		fvco3	$⊢ (G : mREx (T) ⟶ mREx (T) \land y \in mREx (T)) \to (F \circ G) (y) = F (G (y))$
59	39 42 58	syl2anc	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to (F \circ G) (y) = F (G (y))$
60	57 59	oveq12d	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to (F \circ G) (x) ++ (F \circ G) (y) = F (G (x)) ++ F (G (y))$
61	46 55 60	3eqtr4d	$⊢ ((F \in ran S \land G \in ran S) \land (x \in mREx (T) \land y \in mREx (T))) \to (F \circ G) (x ++ y) = (F \circ G) (x) ++ (F \circ G) (y)$
62	61	ralrimivva	$⊢ (F \in ran S \land G \in ran S) \to \forall x \in mREx (T) \forall y \in mREx (T) (F \circ G) (x ++ y) = (F \circ G) (x) ++ (F \circ G) (y)$
63	1 2 21 20	elmrsubrn	$⊢ T \in V \to (F \circ G \in ran S \leftrightarrow ((F \circ G) : mREx (T) ⟶ mREx (T) \land \forall c \in (mCN (T) ∖ mVR (T)) (F \circ G) (⟨“ c ”⟩) = ⟨“ c ”⟩ \land \forall x \in mREx (T) \forall y \in mREx (T) (F \circ G) (x ++ y) = (F \circ G) (x) ++ (F \circ G) (y)))$
64	18 63	syl	$⊢ (F \in ran S \land G \in ran S) \to (F \circ G \in ran S \leftrightarrow ((F \circ G) : mREx (T) ⟶ mREx (T) \land \forall c \in (mCN (T) ∖ mVR (T)) (F \circ G) (⟨“ c ”⟩) = ⟨“ c ”⟩ \land \forall x \in mREx (T) \forall y \in mREx (T) (F \circ G) (x ++ y) = (F \circ G) (x) ++ (F \circ G) (y)))$
65	8 33 62 64	mpbir3and	$⊢ (F \in ran S \land G \in ran S) \to F \circ G \in ran S$

Metamath Proof Explorer

Theorem mrsubco

Proof