frgpnabllem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > frgpnabllem1		Structured version Visualization version Unicode version

Theorem frgpnabllem1 18276

Description: Lemma for frgpnabl 18278. (Contributed by Mario Carneiro, 21-Apr-2016.)

**Hypotheses**
Ref	Expression
frgpnabl.g	freeGrp
frgpnabl.w	Word
frgpnabl.r	~_FG
frgpnabl.p
frgpnabl.m	$\$
frgpnabl.t	splice
frgpnabl.d	$\$
frgpnabl.u	var_FGrp
frgpnabl.i
frgpnabl.a
frgpnabl.b

**Assertion**
Ref	Expression
frgpnabllem1

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem frgpnabllem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frgpnabl.a	. . . . . . 7
2		0ex 4790	. . . . . . . . 9
3	2	prid1 4297	. . . . . . . 8
4		df2o3 7573	. . . . . . . 8
5	3, 4	eleqtrri 2700	. . . . . . 7
6		opelxpi 5148	. . . . . . 7 $/\$
7	1, 5, 6	sylancl 694	. . . . . 6
8		frgpnabl.b	. . . . . . 7
9		opelxpi 5148	. . . . . . 7 $/\$
10	8, 5, 9	sylancl 694	. . . . . 6
11	7, 10	s2cld 13616	. . . . 5 Word
12		frgpnabl.w	. . . . . 6 Word
13		frgpnabl.i	. . . . . . . 8
14		2on 7568	. . . . . . . 8
15		xpexg 6960	. . . . . . . 8 $/\$
16	13, 14, 15	sylancl 694	. . . . . . 7
17		wrdexg 13315	. . . . . . 7 Word
18		fvi 6255	. . . . . . 7 Word Word Word
19	16, 17, 18	3syl 18	. . . . . 6 Word Word
20	12, 19	syl5eq 2668	. . . . 5 Word
21	11, 20	eleqtrrd 2704	. . . 4
22		1n0 7575	. . . . . . 7
23		2cn 11091	. . . . . . . . . . . . . 14
24	23	addid2i 10224	. . . . . . . . . . . . 13
25		s2len 13634	. . . . . . . . . . . . 13
26	24, 25	eqtr4i 2647	. . . . . . . . . . . 12
27		frgpnabl.r	. . . . . . . . . . . . . 14 ~_FG
28		frgpnabl.m	. . . . . . . . . . . . . 14 $\$
29		frgpnabl.t	. . . . . . . . . . . . . 14 splice
30	12, 27, 28, 29	efgtlen 18139	. . . . . . . . . . . . 13 $/\$
31	30	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$
32	26, 31	syl5eq 2668	. . . . . . . . . . 11 $/\$ $/\$
33	32	ex 450	. . . . . . . . . 10 $/\$
34		0cnd 10033	. . . . . . . . . . 11 $/\$
35		simpr 477	. . . . . . . . . . . . . 14 $/\$
36	12	efgrcl 18128	. . . . . . . . . . . . . . . 16 $/\$ Word
37	36	simprd 479	. . . . . . . . . . . . . . 15 Word
38	37	adantl 482	. . . . . . . . . . . . . 14 $/\$ Word
39	35, 38	eleqtrd 2703	. . . . . . . . . . . . 13 $/\$ Word
40		lencl 13324	. . . . . . . . . . . . 13 Word
41	39, 40	syl 17	. . . . . . . . . . . 12 $/\$
42	41	nn0cnd 11353	. . . . . . . . . . 11 $/\$
43		2cnd 11093	. . . . . . . . . . 11 $/\$
44	34, 42, 43	addcan2d 10240	. . . . . . . . . 10 $/\$
45	33, 44	sylibd 229	. . . . . . . . 9 $/\$
46	12, 27, 28, 29	efgtf 18135	. . . . . . . . . . . . . . . . . 18 splice $/\$
47	46	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ splice $/\$
48	47	simpld 475	. . . . . . . . . . . . . . . 16 $/\$ splice
49	48	rneqd 5353	. . . . . . . . . . . . . . 15 $/\$ splice
50	49	eleq2d 2687	. . . . . . . . . . . . . 14 $/\$ splice
51		eqid 2622	. . . . . . . . . . . . . . . 16 splice splice
52		ovex 6678	. . . . . . . . . . . . . . . 16 splice
53	51, 52	elrnmpt2 6773	. . . . . . . . . . . . . . 15 splice splice
54		wrd0 13330	. . . . . . . . . . . . . . . . . . . . 21 Word
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word
56		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
57	28	efgmf 18126	. . . . . . . . . . . . . . . . . . . . . . 23
58	57	ffvelrni 6358	. . . . . . . . . . . . . . . . . . . . . 22
59	56, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
60	56, 59	s2cld 13616	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ Word
61		ccatlid 13369	. . . . . . . . . . . . . . . . . . . . . . . 24 Word ++
62	54, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ++
63	62	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . 22 ++ ++ ++
64	63, 62	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . 21 ++ ++
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ ++ ++
66		simprl 794	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
67		hash0 13158	. . . . . . . . . . . . . . . . . . . . . . . 24
68	67	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . 23
69	66, 68	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
70		elfz1eq 12352	. . . . . . . . . . . . . . . . . . . . . 22
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
72	71, 67	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
73	67	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . 21
74		0cn 10032	. . . . . . . . . . . . . . . . . . . . . . 23
75	71, 74	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
76	75	addid1d 10236	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
77	73, 76	syl5req 2669	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
78	55, 55, 55, 60, 65, 72, 77	splval2 13508	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ splice ++ ++
79		ccatlid 13369	. . . . . . . . . . . . . . . . . . . . . 22 Word ++
80	79	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 Word ++ ++ ++
81		ccatrid 13370	. . . . . . . . . . . . . . . . . . . . 21 Word ++
82	80, 81	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 Word ++ ++
83	60, 82	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ++ ++
84	78, 83	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ splice
85	84	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ splice
86	1	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
87		1on 7567	. . . . . . . . . . . . . . . . . . . 20
88	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
89		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
90	89	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
91		opex 4932	. . . . . . . . . . . . . . . . . . . . . 22
92		s2fv1 13633	. . . . . . . . . . . . . . . . . . . . . 22
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
94		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
95		s2fv1 13633	. . . . . . . . . . . . . . . . . . . . . 22
96	94, 95	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
97	90, 93, 96	3eqtr3g 2679	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
98	89	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
99		opex 4932	. . . . . . . . . . . . . . . . . . . . . . 23
100		s2fv0 13632	. . . . . . . . . . . . . . . . . . . . . . 23
101	99, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
102		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23
103		s2fv0 13632	. . . . . . . . . . . . . . . . . . . . . . 23
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
105	98, 101, 104	3eqtr3g 2679	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
106	105	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
107	28	efgmval 18125	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$
108	86, 5, 107	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\$
109		df-ov 6653	. . . . . . . . . . . . . . . . . . . . 21
110		dif0 3950	. . . . . . . . . . . . . . . . . . . . . 22 $\$
111	110	opeq2i 4406	. . . . . . . . . . . . . . . . . . . . 21 $\$
112	108, 109, 111	3eqtr3g 2679	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
113	97, 106, 112	3eqtr2rd 2663	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
114		opthg 4946	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
115	114	simplbda 654	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
116	86, 88, 113, 115	syl21anc 1325	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
117	116	ex 450	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	85, 117	sylbid 230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ splice
119	118	rexlimdvva 3038	. . . . . . . . . . . . . . 15 $/\$ splice
120	53, 119	syl5bi 232	. . . . . . . . . . . . . 14 $/\$ splice
121	50, 120	sylbid 230	. . . . . . . . . . . . 13 $/\$
122	121	expimpd 629	. . . . . . . . . . . 12 $/\$
123		vex 3203	. . . . . . . . . . . . . . . 16
124		hasheq0 13154	. . . . . . . . . . . . . . . 16
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . 15
126		eleq1 2689	. . . . . . . . . . . . . . . 16
127		fveq2 6191	. . . . . . . . . . . . . . . . . 18
128	127	rneqd 5353	. . . . . . . . . . . . . . . . 17
129	128	eleq2d 2687	. . . . . . . . . . . . . . . 16
130	126, 129	anbi12d 747	. . . . . . . . . . . . . . 15 $/\$ $/\$
131	125, 130	sylbi 207	. . . . . . . . . . . . . 14 $/\$ $/\$
132	131	eqcoms 2630	. . . . . . . . . . . . 13 $/\$ $/\$
133	132	imbi1d 331	. . . . . . . . . . . 12 $/\$ $/\$
134	122, 133	syl5ibrcom 237	. . . . . . . . . . 11 $/\$
135	134	com23 86	. . . . . . . . . 10 $/\$
136	135	expdimp 453	. . . . . . . . 9 $/\$
137	45, 136	mpdd 43	. . . . . . . 8 $/\$
138	137	necon3ad 2807	. . . . . . 7 $/\$
139	22, 138	mpi 20	. . . . . 6 $/\$
140	139	nrexdv 3001	. . . . 5
141		eliun 4524	. . . . 5
142	140, 141	sylnibr 319	. . . 4
143	21, 142	eldifd 3585	. . 3 $\$
144		frgpnabl.d	. . 3 $\$
145	143, 144	syl6eleqr 2712	. 2
146		df-s2 13593	. . . . 5 ++
147	12, 27	efger 18131	. . . . . . 7
148	147	a1i 11	. . . . . 6
149	148, 21	erref 7762	. . . . 5
150	146, 149	syl5eqbrr 4689	. . . 4 ++
151		ovex 6678	. . . . . 6 ++
152	146, 151	eqeltri 2697	. . . . 5
153	152, 151	elec 7786	. . . 4 ++ ++
154	150, 153	sylibr 224	. . 3 ++
155		frgpnabl.u	. . . . . . 7 var_FGrp
156	27, 155	vrgpval 18180	. . . . . 6 $/\$
157	13, 1, 156	syl2anc 693	. . . . 5
158	27, 155	vrgpval 18180	. . . . . 6 $/\$
159	13, 8, 158	syl2anc 693	. . . . 5
160	157, 159	oveq12d 6668	. . . 4
161	7	s1cld 13383	. . . . . 6 Word
162	161, 20	eleqtrrd 2704	. . . . 5
163	10	s1cld 13383	. . . . . 6 Word
164	163, 20	eleqtrrd 2704	. . . . 5
165		frgpnabl.g	. . . . . 6 freeGrp
166		frgpnabl.p	. . . . . 6
167	12, 165, 27, 166	frgpadd 18176	. . . . 5 $/\$ ++
168	162, 164, 167	syl2anc 693	. . . 4 ++
169	160, 168	eqtrd 2656	. . 3 ++
170	154, 169	eleqtrrd 2704	. 2
171	145, 170	elind 3798	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wrex 2913

cvv 3200 $\$ cdif 3571

cin 3573

c0 3915

cpr 4179

cop 4183

cotp 4185

ciun 4520 class class class wbr 4653

cmpt 4729

cid 5023

cxp 5112

crn 5115

con0 5723

wf 5884

cfv 5888 (class class class)co 6650

cmpt2 6652

c1o 7553

c2o 7554

wer 7739

cec 7740

cc 9934

cc0 9936

c1 9937

caddc 9939

c2 11070

cn0 11292

cfz 12326

chash 13117 Word cword 13291 ++ cconcat 13293

cs1 13294 splice csplice 13296

cs2 13586

cplusg 15941 ~_FG cefg 18119 freeGrpcfrgp 18120 var_FGrpcvrgp 18121

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-ot 4186 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-concat 13301 df-s1 13302 df-substr 13303 df-splice 13304 df-s2 13593 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-plusg 15954 df-mulr 15955 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-imas 16168 df-qus 16169 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-frmd 17386 df-efg 18122 df-frgp 18123 df-vrgp 18124

This theorem is referenced by: frgpnabllem2 18277

W3C validator