Step | Hyp | Ref
| Expression |
1 | | mrsubco.s |
. . . . 5
⊢ 𝑆 = (mRSubst‘𝑇) |
2 | | eqid 2610 |
. . . . 5
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
3 | 1, 2 | mrsubf 30668 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:(mREx‘𝑇)⟶(mREx‘𝑇)) |
4 | 3 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → 𝐹:(mREx‘𝑇)⟶(mREx‘𝑇)) |
5 | 1, 2 | mrsubf 30668 |
. . . 4
⊢ (𝐺 ∈ ran 𝑆 → 𝐺:(mREx‘𝑇)⟶(mREx‘𝑇)) |
6 | 5 | adantl 481 |
. . 3
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → 𝐺:(mREx‘𝑇)⟶(mREx‘𝑇)) |
7 | | fco 5971 |
. . 3
⊢ ((𝐹:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ 𝐺:(mREx‘𝑇)⟶(mREx‘𝑇)) → (𝐹 ∘ 𝐺):(mREx‘𝑇)⟶(mREx‘𝑇)) |
8 | 4, 6, 7 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺):(mREx‘𝑇)⟶(mREx‘𝑇)) |
9 | 6 | adantr 480 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → 𝐺:(mREx‘𝑇)⟶(mREx‘𝑇)) |
10 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇)) → 𝑐 ∈ (mCN‘𝑇)) |
11 | | elun1 3742 |
. . . . . . . . 9
⊢ (𝑐 ∈ (mCN‘𝑇) → 𝑐 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇)) → 𝑐 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → 𝑐 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
14 | 13 | s1cld 13236 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → 〈“𝑐”〉 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
15 | | n0i 3879 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
16 | | fvprc 6097 |
. . . . . . . . . . . . 13
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
17 | 1, 16 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
18 | 17 | rneqd 5274 |
. . . . . . . . . . 11
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
19 | | rn0 5298 |
. . . . . . . . . . 11
⊢ ran
∅ = ∅ |
20 | 18, 19 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
21 | 15, 20 | nsyl2 141 |
. . . . . . . . 9
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
22 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → 𝑇 ∈ V) |
23 | 22 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → 𝑇 ∈ V) |
24 | | eqid 2610 |
. . . . . . . 8
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
25 | | eqid 2610 |
. . . . . . . 8
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
26 | 24, 25, 2 | mrexval 30652 |
. . . . . . 7
⊢ (𝑇 ∈ V →
(mREx‘𝑇) = Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
27 | 23, 26 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
28 | 14, 27 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → 〈“𝑐”〉 ∈ (mREx‘𝑇)) |
29 | | fvco3 6185 |
. . . . 5
⊢ ((𝐺:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ 〈“𝑐”〉 ∈ (mREx‘𝑇)) → ((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = (𝐹‘(𝐺‘〈“𝑐”〉))) |
30 | 9, 28, 29 | syl2anc 691 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → ((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = (𝐹‘(𝐺‘〈“𝑐”〉))) |
31 | 1, 2, 25, 24 | mrsubcn 30670 |
. . . . . 6
⊢ ((𝐺 ∈ ran 𝑆 ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (𝐺‘〈“𝑐”〉) = 〈“𝑐”〉) |
32 | 31 | adantll 746 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (𝐺‘〈“𝑐”〉) = 〈“𝑐”〉) |
33 | 32 | fveq2d 6107 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (𝐹‘(𝐺‘〈“𝑐”〉)) = (𝐹‘〈“𝑐”〉)) |
34 | 1, 2, 25, 24 | mrsubcn 30670 |
. . . . 5
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
35 | 34 | adantlr 747 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → (𝐹‘〈“𝑐”〉) = 〈“𝑐”〉) |
36 | 30, 33, 35 | 3eqtrd 2648 |
. . 3
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ 𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))) → ((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = 〈“𝑐”〉) |
37 | 36 | ralrimiva 2949 |
. 2
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → ∀𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = 〈“𝑐”〉) |
38 | 1, 2 | mrsubccat 30669 |
. . . . . . . 8
⊢ ((𝐺 ∈ ran 𝑆 ∧ 𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇)) → (𝐺‘(𝑥 ++ 𝑦)) = ((𝐺‘𝑥) ++ (𝐺‘𝑦))) |
39 | 38 | 3expb 1258 |
. . . . . . 7
⊢ ((𝐺 ∈ ran 𝑆 ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐺‘(𝑥 ++ 𝑦)) = ((𝐺‘𝑥) ++ (𝐺‘𝑦))) |
40 | 39 | adantll 746 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐺‘(𝑥 ++ 𝑦)) = ((𝐺‘𝑥) ++ (𝐺‘𝑦))) |
41 | 40 | fveq2d 6107 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐹‘(𝐺‘(𝑥 ++ 𝑦))) = (𝐹‘((𝐺‘𝑥) ++ (𝐺‘𝑦)))) |
42 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝐹 ∈ ran 𝑆) |
43 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝐺:(mREx‘𝑇)⟶(mREx‘𝑇)) |
44 | | simprl 790 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝑥 ∈ (mREx‘𝑇)) |
45 | 43, 44 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐺‘𝑥) ∈ (mREx‘𝑇)) |
46 | | simprr 792 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝑦 ∈ (mREx‘𝑇)) |
47 | 43, 46 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐺‘𝑦) ∈ (mREx‘𝑇)) |
48 | 1, 2 | mrsubccat 30669 |
. . . . . 6
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝐺‘𝑥) ∈ (mREx‘𝑇) ∧ (𝐺‘𝑦) ∈ (mREx‘𝑇)) → (𝐹‘((𝐺‘𝑥) ++ (𝐺‘𝑦))) = ((𝐹‘(𝐺‘𝑥)) ++ (𝐹‘(𝐺‘𝑦)))) |
49 | 42, 45, 47, 48 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐹‘((𝐺‘𝑥) ++ (𝐺‘𝑦))) = ((𝐹‘(𝐺‘𝑥)) ++ (𝐹‘(𝐺‘𝑦)))) |
50 | 41, 49 | eqtrd 2644 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝐹‘(𝐺‘(𝑥 ++ 𝑦))) = ((𝐹‘(𝐺‘𝑥)) ++ (𝐹‘(𝐺‘𝑦)))) |
51 | 22, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
52 | 51 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (mREx‘𝑇) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
53 | 44, 52 | eleqtrd 2690 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝑥 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
54 | 46, 52 | eleqtrd 2690 |
. . . . . . 7
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
55 | | ccatcl 13212 |
. . . . . . 7
⊢ ((𝑥 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑦 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (𝑥 ++ 𝑦) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
56 | 53, 54, 55 | syl2anc 691 |
. . . . . 6
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝑥 ++ 𝑦) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) |
57 | 56, 52 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (𝑥 ++ 𝑦) ∈ (mREx‘𝑇)) |
58 | | fvco3 6185 |
. . . . 5
⊢ ((𝐺:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ (𝑥 ++ 𝑦) ∈ (mREx‘𝑇)) → ((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (𝐹‘(𝐺‘(𝑥 ++ 𝑦)))) |
59 | 43, 57, 58 | syl2anc 691 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → ((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (𝐹‘(𝐺‘(𝑥 ++ 𝑦)))) |
60 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐺:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ 𝑥 ∈ (mREx‘𝑇)) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) |
61 | 43, 44, 60 | syl2anc 691 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) |
62 | | fvco3 6185 |
. . . . . 6
⊢ ((𝐺:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇)) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) |
63 | 43, 46, 62 | syl2anc 691 |
. . . . 5
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) |
64 | 61, 63 | oveq12d 6567 |
. . . 4
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → (((𝐹 ∘ 𝐺)‘𝑥) ++ ((𝐹 ∘ 𝐺)‘𝑦)) = ((𝐹‘(𝐺‘𝑥)) ++ (𝐹‘(𝐺‘𝑦)))) |
65 | 50, 59, 64 | 3eqtr4d 2654 |
. . 3
⊢ (((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) ∧ (𝑥 ∈ (mREx‘𝑇) ∧ 𝑦 ∈ (mREx‘𝑇))) → ((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (((𝐹 ∘ 𝐺)‘𝑥) ++ ((𝐹 ∘ 𝐺)‘𝑦))) |
66 | 65 | ralrimivva 2954 |
. 2
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → ∀𝑥 ∈ (mREx‘𝑇)∀𝑦 ∈ (mREx‘𝑇)((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (((𝐹 ∘ 𝐺)‘𝑥) ++ ((𝐹 ∘ 𝐺)‘𝑦))) |
67 | 1, 2, 25, 24 | elmrsubrn 30671 |
. . 3
⊢ (𝑇 ∈ V → ((𝐹 ∘ 𝐺) ∈ ran 𝑆 ↔ ((𝐹 ∘ 𝐺):(mREx‘𝑇)⟶(mREx‘𝑇) ∧ ∀𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈
(mREx‘𝑇)∀𝑦 ∈ (mREx‘𝑇)((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (((𝐹 ∘ 𝐺)‘𝑥) ++ ((𝐹 ∘ 𝐺)‘𝑦))))) |
68 | 22, 67 | syl 17 |
. 2
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → ((𝐹 ∘ 𝐺) ∈ ran 𝑆 ↔ ((𝐹 ∘ 𝐺):(mREx‘𝑇)⟶(mREx‘𝑇) ∧ ∀𝑐 ∈ ((mCN‘𝑇) ∖ (mVR‘𝑇))((𝐹 ∘ 𝐺)‘〈“𝑐”〉) = 〈“𝑐”〉 ∧
∀𝑥 ∈
(mREx‘𝑇)∀𝑦 ∈ (mREx‘𝑇)((𝐹 ∘ 𝐺)‘(𝑥 ++ 𝑦)) = (((𝐹 ∘ 𝐺)‘𝑥) ++ ((𝐹 ∘ 𝐺)‘𝑦))))) |
69 | 8, 37, 66, 68 | mpbir3and 1238 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |