Metamath Proof Explorer

Theorem wlkiswwlks2lem4

Description: Lemma 4 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 10-Apr-2021)

Ref Expression
Hypotheses wlkiswwlks2lem.f ⊢F=x∈0..^P−1⟼E-1⁡P⁡xP⁡x+1
wlkiswwlks2lem.e ⊢E=iEdg⁡G
Assertion wlkiswwlks2lem4 ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢F=x∈0..^P−1⟼E-1⁡P⁡xP⁡x+1
2 wlkiswwlks2lem.e ⊢E=iEdg⁡G
3 1 wlkiswwlks2lem1 ⊢P∈WordV∧1≤P→F=P−1
4 3 3adant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→F=P−1
5 lencl ⊢P∈WordV→P∈ℕ0
6 5 3ad2ant2 ⊢G∈USHGraph∧P∈WordV∧1≤P→P∈ℕ0
7 1 wlkiswwlks2lem2 ⊢P∈ℕ0∧i∈0..^P−1→F⁡i=E-1⁡P⁡iP⁡i+1
8 6 7 sylan ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1→F⁡i=E-1⁡P⁡iP⁡i+1
9 8 adantr ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1∧P⁡iP⁡i+1∈ran⁡E→F⁡i=E-1⁡P⁡iP⁡i+1
10 9 fveq2d ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1∧P⁡iP⁡i+1∈ran⁡E→E⁡F⁡i=E⁡E-1⁡P⁡iP⁡i+1
11 2 uspgrf1oedg ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoEdg⁡G
12 2 rneqi ⊢ran⁡E=ran⁡iEdg⁡G
13 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
14 12 13 eqtr4i ⊢ran⁡E=Edg⁡G
15 f1oeq3 ⊢ran⁡E=Edg⁡G→E:dom⁡E⟶1-1 ontoran⁡E↔E:dom⁡E⟶1-1 ontoEdg⁡G
16 14 15 ax-mp ⊢E:dom⁡E⟶1-1 ontoran⁡E↔E:dom⁡E⟶1-1 ontoEdg⁡G
17 11 16 sylibr ⊢G∈USHGraph→E:dom⁡E⟶1-1 ontoran⁡E
18 17 3ad2ant1 ⊢G∈USHGraph∧P∈WordV∧1≤P→E:dom⁡E⟶1-1 ontoran⁡E
19 18 adantr ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1→E:dom⁡E⟶1-1 ontoran⁡E
20 f1ocnvfv2 ⊢E:dom⁡E⟶1-1 ontoran⁡E∧P⁡iP⁡i+1∈ran⁡E→E⁡E-1⁡P⁡iP⁡i+1=P⁡iP⁡i+1
21 19 20 sylan ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1∧P⁡iP⁡i+1∈ran⁡E→E⁡E-1⁡P⁡iP⁡i+1=P⁡iP⁡i+1
22 10 21 eqtrd ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1∧P⁡iP⁡i+1∈ran⁡E→E⁡F⁡i=P⁡iP⁡i+1
23 22 ex ⊢G∈USHGraph∧P∈WordV∧1≤P∧i∈0..^P−1→P⁡iP⁡i+1∈ran⁡E→E⁡F⁡i=P⁡iP⁡i+1
24 23 ralimdva ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
25 oveq2 ⊢F=P−1→0..^F=0..^P−1
26 25 raleqdv ⊢F=P−1→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
27 26 imbi2d ⊢F=P−1→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1↔∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^P−1E⁡F⁡i=P⁡iP⁡i+1
28 24 27 syl5ibr ⊢F=P−1→G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1
29 4 28 mpcom ⊢G∈USHGraph∧P∈WordV∧1≤P→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E→∀i∈0..^FE⁡F⁡i=P⁡iP⁡i+1