Metamath Proof Explorer

Theorem mrsubco

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

Ref Expression
Hypothesis mrsubco.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsubco ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 )

Proof

Step Hyp Ref Expression
1 mrsubco.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
2 eqid ⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
3 1 2 mrsubf ⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
4 3 adantr ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → 𝐹 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
5 1 2 mrsubf ⊢ ( 𝐺 ∈ ran 𝑆 → 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
6 5 adantl ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
7 fco ⊢ ( ( 𝐹 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
8 4 6 7 syl2anc ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( 𝐹 ∘ 𝐺 ) : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
9 6 adantr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
10 eldifi ⊢ ( 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) → 𝑐 ∈ ( mCN ‘ 𝑇 ) )
11 elun1 ⊢ ( 𝑐 ∈ ( mCN ‘ 𝑇 ) → 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
12 10 11 syl ⊢ ( 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) → 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
13 12 adantl ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
14 13 s1cld ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ⟨“ 𝑐 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
15 n0i ⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ )
16 1 rnfvprc ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
17 15 16 nsyl2 ⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V )
18 17 adantr ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → 𝑇 ∈ V )
19 18 adantr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → 𝑇 ∈ V )
20 eqid ⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
21 eqid ⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
22 20 21 2 mrexval ⊢ ( 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
23 19 22 syl ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
24 14 23 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ⟨“ 𝑐 ”⟩ ∈ ( mREx ‘ 𝑇 ) )
25 fvco3 ⊢ ( ( 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ⟨“ 𝑐 ”⟩ ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ( 𝐹 ‘ ( 𝐺 ‘ ⟨“ 𝑐 ”⟩ ) ) )
26 9 24 25 syl2anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ( 𝐹 ‘ ( 𝐺 ‘ ⟨“ 𝑐 ”⟩ ) ) )
27 1 2 21 20 mrsubcn ⊢ ( ( 𝐺 ∈ ran 𝑆 ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( 𝐺 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
28 27 adantll ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( 𝐺 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
29 28 fveq2d ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ⟨“ 𝑐 ”⟩ ) ) = ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) )
30 1 2 21 20 mrsubcn ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
31 30 adantlr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
32 26 29 31 3eqtrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
33 32 ralrimiva ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ∀ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ )
34 1 2 mrsubccat ⊢ ( ( 𝐺 ∈ ran 𝑆 ∧ 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) → ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) )
35 34 3expb ⊢ ( ( 𝐺 ∈ ran 𝑆 ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) )
36 35 adantll ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) )
37 36 fveq2d ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) ) )
38 simpll ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝐹 ∈ ran 𝑆 )
39 6 adantr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
40 simprl ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝑥 ∈ ( mREx ‘ 𝑇 ) )
41 39 40 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( mREx ‘ 𝑇 ) )
42 simprr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝑦 ∈ ( mREx ‘ 𝑇 ) )
43 39 42 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) )
44 1 2 mrsubccat ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( mREx ‘ 𝑇 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ++ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
45 38 41 43 44 syl3anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ++ ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ++ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
46 37 45 eqtrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ++ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
47 18 22 syl ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
48 47 adantr ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
49 40 48 eleqtrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝑥 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
50 42 48 eleqtrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → 𝑦 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
51 ccatcl ⊢ ( ( 𝑥 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∧ 𝑦 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( 𝑥 ++ 𝑦 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
52 49 50 51 syl2anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝑥 ++ 𝑦 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
53 52 48 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( 𝑥 ++ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) )
54 fvco3 ⊢ ( ( 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ( 𝑥 ++ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) ) )
55 39 53 54 syl2anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ++ 𝑦 ) ) ) )
56 fvco3 ⊢ ( ( 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ 𝑥 ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
57 39 40 56 syl2anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
58 fvco3 ⊢ ( ( 𝐺 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
59 39 42 58 syl2anc ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
60 57 59 oveq12d ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ++ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ++ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
61 46 55 60 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) ∧ ( 𝑥 ∈ ( mREx ‘ 𝑇 ) ∧ 𝑦 ∈ ( mREx ‘ 𝑇 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ++ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
62 61 ralrimivva ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ∀ 𝑥 ∈ ( mREx ‘ 𝑇 ) ∀ 𝑦 ∈ ( mREx ‘ 𝑇 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ++ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
63 1 2 21 20 elmrsubrn ⊢ ( 𝑇 ∈ V → ( ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ↔ ( ( 𝐹 ∘ 𝐺 ) : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ∀ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ ( mREx ‘ 𝑇 ) ∀ 𝑦 ∈ ( mREx ‘ 𝑇 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ++ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
64 18 63 syl ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ↔ ( ( 𝐹 ∘ 𝐺 ) : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ∀ 𝑐 ∈ ( ( mCN ‘ 𝑇 ) ∖ ( mVR ‘ 𝑇 ) ) ( ( 𝐹 ∘ 𝐺 ) ‘ ⟨“ 𝑐 ”⟩ ) = ⟨“ 𝑐 ”⟩ ∧ ∀ 𝑥 ∈ ( mREx ‘ 𝑇 ) ∀ 𝑦 ∈ ( mREx ‘ 𝑇 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ++ 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ++ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
65 8 33 62 64 mpbir3and ⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 )