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

Theorem efgredlemg 15366
 Description: Lemma for efgred 15372. (Contributed by Mario Carneiro, 4-Jun-2016.)
Hypotheses
Ref Expression
efgval.w Word
efgval.r ~FG
efgval2.m
efgval2.t splice
efgred.d
efgred.s Word ..^
efgredlem.1
efgredlem.2
efgredlem.3
efgredlem.4
efgredlem.5
efgredlemb.k
efgredlemb.l
efgredlemb.p
efgredlemb.q
efgredlemb.u
efgredlemb.v
efgredlemb.6
efgredlemb.7
Assertion
Ref Expression
efgredlemg
Distinct variable groups:   ,,   ,,,   ,,   ,,   ,,,,,,   ,,,,,,,,   ,,,,,   ,,,,,,   ,,,,,   ,,,,,,   ,,   ,,,,,,,,,   ,,,,,,,   ,,   ,,   ,,,,,,,,,,   ,,,,
Allowed substitution hints:   (,,,,,,,,,,)   (,,,,,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,,,,,)   (,,,,)   (,,,,,)   ()   (,,,,,,,,)   (,,,,,,,,)   (,,)   (,,,,,)

Proof of Theorem efgredlemg
StepHypRef Expression
1 efgval.w . . . . . 6 Word
2 fviss 5776 . . . . . 6 Word Word
31, 2eqsstri 3370 . . . . 5 Word
4 efgval.r . . . . . . 7 ~FG
5 efgval2.m . . . . . . 7
6 efgval2.t . . . . . . 7 splice
7 efgred.d . . . . . . 7
8 efgred.s . . . . . . 7 Word ..^
9 efgredlem.1 . . . . . . 7
10 efgredlem.2 . . . . . . 7
11 efgredlem.3 . . . . . . 7
12 efgredlem.4 . . . . . . 7
13 efgredlem.5 . . . . . . 7
14 efgredlemb.k . . . . . . 7
15 efgredlemb.l . . . . . . 7
161, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15efgredlemf 15365 . . . . . 6
1716simpld 446 . . . . 5
183, 17sseldi 3338 . . . 4 Word
19 lencl 11727 . . . 4 Word
2018, 19syl 16 . . 3
2120nn0cnd 10268 . 2
2216simprd 450 . . . . 5
233, 22sseldi 3338 . . . 4 Word
24 lencl 11727 . . . 4 Word
2523, 24syl 16 . . 3
2625nn0cnd 10268 . 2
27 2cn 10062 . . 3
2827a1i 11 . 2
291, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13efgredlema 15364 . . . . . . 7
3029simpld 446 . . . . . 6
311, 4, 5, 6, 7, 8efgsdmi 15356 . . . . . 6
3210, 30, 31syl2anc 643 . . . . 5
3314fveq2i 5723 . . . . . . 7
3433fveq2i 5723 . . . . . 6
3534rneqi 5088 . . . . 5
3632, 35syl6eleqr 2526 . . . 4
371, 4, 5, 6efgtlen 15350 . . . 4
3817, 36, 37syl2anc 643 . . 3
3929simprd 450 . . . . . . 7
401, 4, 5, 6, 7, 8efgsdmi 15356 . . . . . . 7
4111, 39, 40syl2anc 643 . . . . . 6
4212, 41eqeltrd 2509 . . . . 5
4315fveq2i 5723 . . . . . . 7
4443fveq2i 5723 . . . . . 6
4544rneqi 5088 . . . . 5
4642, 45syl6eleqr 2526 . . . 4
471, 4, 5, 6efgtlen 15350 . . . 4
4822, 46, 47syl2anc 643 . . 3
4938, 48eqtr3d 2469 . 2