Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elmrsubrn Structured version   Unicode version

Theorem elmrsubrn 30110
 Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses because we don't know that and are disjoint until we get to ismfs 30139.) (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mrsubccat.s mRSubst
mrsubccat.r mREx
mrsubcn.v mVR
mrsubcn.c mCN
Assertion
Ref Expression
elmrsubrn ++ ++
Distinct variable groups:   ,,,   ,,   ,,,   ,,   ,,,   ,,,   ,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem elmrsubrn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mrsubccat.s . . . 4 mRSubst
2 mrsubccat.r . . . 4 mREx
31, 2mrsubf 30107 . . 3
4 mrsubcn.v . . . . 5 mVR
5 mrsubcn.c . . . . 5 mCN
61, 2, 4, 5mrsubcn 30109 . . . 4
76ralrimiva 2779 . . 3
81, 2mrsubccat 30108 . . . . 5 ++ ++
983expb 1206 . . . 4 ++ ++
109ralrimivva 2786 . . 3 ++ ++
113, 7, 103jca 1185 . 2 ++ ++
125, 4, 2mrexval 30091 . . . . . . 7 Word
1312adantr 466 . . . . . 6 ++ ++ Word
14 s1eq 12687 . . . . . . . . . . . . 13
1514fveq2d 5829 . . . . . . . . . . . 12
16 eqid 2428 . . . . . . . . . . . 12
17 fvex 5835 . . . . . . . . . . . 12
1815, 16, 17fvmpt 5908 . . . . . . . . . . 11
1918adantl 467 . . . . . . . . . 10 ++ ++
20 difun2 3820 . . . . . . . . . . . . . . 15
2120eleq2i 2498 . . . . . . . . . . . . . 14
22 eldif 3389 . . . . . . . . . . . . . 14
2321, 22bitr3i 254 . . . . . . . . . . . . 13
24 simpr2 1012 . . . . . . . . . . . . . 14 ++ ++
25 s1eq 12687 . . . . . . . . . . . . . . . . 17
2625fveq2d 5829 . . . . . . . . . . . . . . . 16
2726, 25eqeq12d 2443 . . . . . . . . . . . . . . 15
2827rspccva 3124 . . . . . . . . . . . . . 14
2924, 28sylan 473 . . . . . . . . . . . . 13 ++ ++
3023, 29sylan2br 478 . . . . . . . . . . . 12 ++ ++
3130anassrs 652 . . . . . . . . . . 11 ++ ++
3231eqcomd 2434 . . . . . . . . . 10 ++ ++
3319, 32ifeqda 3887 . . . . . . . . 9 ++ ++
3433mpteq2dva 4453 . . . . . . . 8 ++ ++
3534coeq1d 4958 . . . . . . 7 ++ ++
3635oveq2d 6265 . . . . . 6 ++ ++ freeMnd g freeMnd g
3713, 36mpteq12dv 4445 . . . . 5 ++ ++ freeMnd g Word freeMnd g
38 elun2 3577 . . . . . . . 8
39 simpr1 1011 . . . . . . . . . 10 ++ ++
4039adantr 466 . . . . . . . . 9 ++ ++
41 simpr 462 . . . . . . . . . . 11 ++ ++
4241s1cld 12690 . . . . . . . . . 10 ++ ++ Word
4312ad2antrr 730 . . . . . . . . . 10 ++ ++ Word
4442, 43eleqtrrd 2509 . . . . . . . . 9 ++ ++
4540, 44ffvelrnd 5982 . . . . . . . 8 ++ ++
4638, 45sylan2 476 . . . . . . 7 ++ ++
4715cbvmptv 4459 . . . . . . 7
4846, 47fmptd 6005 . . . . . 6 ++ ++
49 ssid 3426 . . . . . 6
50 eqid 2428 . . . . . . 7 freeMnd freeMnd
515, 4, 2, 1, 50mrsubfval 30098 . . . . . 6 freeMnd g
5248, 49, 51sylancl 666 . . . . 5 ++ ++ freeMnd g
53 fvex 5835 . . . . . . . . . 10 mCN
545, 53eqeltri 2502 . . . . . . . . 9
55 fvex 5835 . . . . . . . . . 10 mVR
564, 55eqeltri 2502 . . . . . . . . 9
5754, 56unex 6547 . . . . . . . 8
5850frmdmnd 16586 . . . . . . . 8 freeMnd
5957, 58ax-mp 5 . . . . . . 7 freeMnd
6059a1i 11 . . . . . 6 ++ ++ freeMnd
6157a1i 11 . . . . . 6 ++ ++
6245, 43eleqtrd 2508 . . . . . . 7 ++ ++ Word
63 eqid 2428 . . . . . . 7
6462, 63fmptd 6005 . . . . . 6 ++ ++ Word
6513, 13feq23d 5684 . . . . . . . 8 ++ ++ Word Word
6639, 65mpbid 213 . . . . . . 7 ++ ++ Word Word
67 simpr3 1013 . . . . . . . 8 ++ ++ ++ ++
68 simprl 762 . . . . . . . . . . . . . . 15
6912adantr 466 . . . . . . . . . . . . . . . 16 Word
7069adantr 466 . . . . . . . . . . . . . . 15 Word
7168, 70eleqtrd 2508 . . . . . . . . . . . . . 14 Word
72 simprr 764 . . . . . . . . . . . . . . 15
7372, 70eleqtrd 2508 . . . . . . . . . . . . . 14 Word
74 eqid 2428 . . . . . . . . . . . . . . . . . 18 freeMnd freeMnd
7550, 74frmdbas 16579 . . . . . . . . . . . . . . . . 17 freeMnd Word
7657, 75ax-mp 5 . . . . . . . . . . . . . . . 16 freeMnd Word
7776eqcomi 2437 . . . . . . . . . . . . . . 15 Word freeMnd
78 eqid 2428 . . . . . . . . . . . . . . 15 freeMnd freeMnd
7950, 77, 78frmdadd 16582 . . . . . . . . . . . . . 14 Word Word freeMnd ++
8071, 73, 79syl2anc 665 . . . . . . . . . . . . 13 freeMnd ++
8180fveq2d 5829 . . . . . . . . . . . 12 freeMnd ++
82 ffvelrn 5979 . . . . . . . . . . . . . . 15
8382ad2ant2lr 752 . . . . . . . . . . . . . 14
8483, 70eleqtrd 2508 . . . . . . . . . . . . 13 Word
85 ffvelrn 5979 . . . . . . . . . . . . . . 15
8685ad2ant2l 750 . . . . . . . . . . . . . 14
8786, 70eleqtrd 2508 . . . . . . . . . . . . 13 Word
8850, 77, 78frmdadd 16582 . . . . . . . . . . . . 13 Word Word freeMnd ++
8984, 87, 88syl2anc 665 . . . . . . . . . . . 12 freeMnd ++
9081, 89eqeq12d 2443 . . . . . . . . . . 11 freeMnd freeMnd ++ ++
91902ralbidva 2807 . . . . . . . . . 10 freeMnd freeMnd ++ ++
9269raleqdv 2970 . . . . . . . . . . 11 freeMnd freeMnd Word freeMnd freeMnd
9369, 92raleqbidv 2978 . . . . . . . . . 10 freeMnd freeMnd Word Word freeMnd freeMnd
9491, 93bitr3d 258 . . . . . . . . 9 ++ ++ Word Word freeMnd freeMnd
95943ad2antr1 1170 . . . . . . . 8 ++ ++ ++ ++ Word Word freeMnd freeMnd
9667, 95mpbid 213 . . . . . . 7 ++ ++ Word Word freeMnd freeMnd
97 wrd0 12639 . . . . . . . . . . . 12 Word
98 ffvelrn 5979 . . . . . . . . . . . 12 Word Word Word Word
9966, 97, 98sylancl 666 . . . . . . . . . . 11 ++ ++ Word
100 lencl 12635 . . . . . . . . . . 11 Word
10199, 100syl 17 . . . . . . . . . 10 ++ ++
102101nn0cnd 10878 . . . . . . . . 9 ++ ++
103 0cnd 9587 . . . . . . . . 9 ++ ++
104102addid1d 9784 . . . . . . . . . 10 ++ ++
10597, 13syl5eleqr 2513 . . . . . . . . . . . 12 ++ ++
106 oveq1 6256 . . . . . . . . . . . . . . 15 ++ ++
107106fveq2d 5829 . . . . . . . . . . . . . 14 ++ ++
108 fveq2 5825 . . . . . . . . . . . . . . 15
109108oveq1d 6264 . . . . . . . . . . . . . 14 ++ ++
110107, 109eqeq12d 2443 . . . . . . . . . . . . 13 ++ ++ ++ ++
111 oveq2 6257 . . . . . . . . . . . . . . . 16 ++ ++
112 ccatlid 12678 . . . . . . . . . . . . . . . . 17 Word ++
11397, 112ax-mp 5 . . . . . . . . . . . . . . . 16 ++
114111, 113syl6eq 2478 . . . . . . . . . . . . . . 15 ++
115114fveq2d 5829 . . . . . . . . . . . . . 14 ++
116 fveq2 5825 . . . . . . . . . . . . . . 15
117116oveq2d 6265 . . . . . . . . . . . . . 14 ++ ++
118115, 117eqeq12d 2443 . . . . . . . . . . . . 13 ++ ++ ++
119110, 118rspc2va 3135 . . . . . . . . . . . 12 ++ ++ ++
120105, 105, 67, 119syl21anc 1263 . . . . . . . . . . 11 ++ ++ ++
121120fveq2d 5829 . . . . . . . . . 10 ++ ++ ++
122 ccatlen 12669 . . . . . . . . . . 11 Word Word ++
12399, 99, 122syl2anc 665 . . . . . . . . . 10 ++ ++ ++
124104, 121, 1233eqtrrd 2467 . . . . . . . . 9 ++ ++
125102, 102, 103, 124addcanad 9789 . . . . . . . 8 ++ ++
126 fvex 5835 . . . . . . . . 9
127 hasheq0 12494 . . . . . . . . 9
128126, 127ax-mp 5 . . . . . . . 8
129125, 128sylib 199 . . . . . . 7 ++ ++
13059, 59pm3.2i 456 . . . . . . . 8 freeMnd freeMnd
13150frmd0 16587 . . . . . . . . 9 freeMnd
13277, 77, 78, 78, 131, 131ismhm 16527 . . . . . . . 8 freeMnd MndHom freeMnd freeMnd freeMnd Word Word Word Word freeMnd freeMnd
133130, 132mpbiran 926 . . . . . . 7 freeMnd MndHom freeMnd Word Word Word Word freeMnd freeMnd
13466, 96, 129, 133syl3anbrc 1189 . . . . . 6 ++ ++ freeMnd MndHom freeMnd
135 eqid 2428 . . . . . . . . . 10 varFMnd varFMnd
136135vrmdf 16585 . . . . . . . . 9 varFMnd Word
13757, 136ax-mp 5 . . . . . . . 8 varFMnd Word
138 fcompt 6018 . . . . . . . 8 Word Word varFMnd Word varFMnd varFMnd
13966, 137, 138sylancl 666 . . . . . . 7 ++ ++ varFMnd varFMnd
140135vrmdval 16584 . . . . . . . . . 10 varFMnd
14161, 140sylan 473 . . . . . . . . 9 ++ ++ varFMnd
142141fveq2d 5829 . . . . . . . 8 ++ ++ varFMnd
143142mpteq2dva 4453 . . . . . . 7 ++ ++ varFMnd
144139, 143eqtrd 2462 . . . . . 6 ++ ++ varFMnd
14550, 77, 135frmdup3lem 16593 . . . . . 6 freeMnd Word freeMnd MndHom freeMnd varFMnd Word freeMnd g
14660, 61, 64, 134, 144, 145syl32anc 1272 . . . . 5 ++ ++ Word freeMnd g
14737, 52, 1463eqtr4rd 2473 . . . 4 ++ ++
1484, 2, 1mrsubff 30102 . . . . . . 7
149 ffn 5689 . . . . . . 7
150148, 149syl 17 . . . . . 6
151150adantr 466 . . . . 5 ++ ++
152 fvex 5835 . . . . . . . 8 mREx
1532, 152eqeltri 2502 . . . . . . 7
154 elpm2r 7444 . . . . . . 7
155153, 56, 154mpanl12 686 . . . . . 6
15648, 49, 155sylancl 666 . . . . 5 ++ ++
157 fnfvelrn 5978 . . . . 5
158151, 156, 157syl2anc 665 . . . 4 ++ ++
159147, 158eqeltrd 2506 . . 3 ++ ++
160159ex 435 . 2 ++ ++
16111, 160impbid2 207 1 ++ ++
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2714  cvv 3022   cdif 3376   cun 3377   wss 3379  c0 3704  cif 3854   cmpt 4425   crn 4797   ccom 4800   wfn 5539  wf 5540  cfv 5544  (class class class)co 6249   cmap 7427   cpm 7428  cc0 9490   caddc 9493  cn0 10820  chash 12465  Word cword 12604   ++ cconcat 12606  cs1 12607  cbs 15064   cplusg 15133   g cgsu 15282  cmnd 16478   MndHom cmhm 16523  freeMndcfrmd 16574  varFMndcvrmd 16575  mCNcmcn 30050  mVRcmvar 30051  mRExcmrex 30056  mRSubstcmrsub 30060 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-card 8325  df-cda 8549  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-n0 10821  df-z 10889  df-uz 11111  df-fz 11736  df-fzo 11867  df-seq 12164  df-hash 12466  df-word 12612  df-lsw 12613  df-concat 12614  df-s1 12615  df-substr 12616  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-plusg 15146  df-0g 15283  df-gsum 15284  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-mhm 16525  df-submnd 16526  df-frmd 16576  df-vrmd 16577  df-mrex 30076  df-mrsub 30080 This theorem is referenced by:  mrsubco  30111
 Copyright terms: Public domain W3C validator