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

Theorem clwwlkccatlem 28353
Description: Lemma for clwwlkccat 28354: index 𝑗 is shifted up by (♯‘𝐴), and the case 𝑖 = ((♯‘𝐴) − 1) is covered by the "bridge" {(lastS‘𝐴), (𝐵‘0)} = {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺). (Contributed by AV, 23-Apr-2022.)
Assertion
Ref Expression
clwwlkccatlem ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝐴 ++ 𝐵)) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
Distinct variable groups:   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗   𝑖,𝐺,𝑗

Proof of Theorem clwwlkccatlem
StepHypRef Expression
1 simplll 772 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐴 ∈ Word (Vtx‘𝐺))
2 simplr 766 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺))
3 lencl 14236 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈ ℕ0)
43nn0zd 12424 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈ ℤ)
5 fzossrbm1 13416 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐴) ∈ ℤ → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
64, 5syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Word (Vtx‘𝐺) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
76ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
87sselda 3921 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
9 ccatval1 14281 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴𝑖))
101, 2, 8, 9syl3anc 1370 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴𝑖))
114ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘𝐴) ∈ ℤ)
12 elfzom1elp1fzo 13454 . . . . . . . . . . . . . . . . . 18 (((♯‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
1311, 12sylan 580 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
14 ccatval1 14281 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1)))
151, 2, 13, 14syl3anc 1370 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1)))
1610, 15preq12d 4677 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐴𝑖), (𝐴‘(𝑖 + 1))})
1716eleq1d 2823 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1817biimprd 247 . . . . . . . . . . . . 13 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1918ralimdva 3108 . . . . . . . . . . . 12 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2019impancom 452 . . . . . . . . . . 11 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝐵 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
21203adant3 1131 . . . . . . . . . 10 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (𝐵 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2221com12 32 . . . . . . . . 9 (𝐵 ∈ Word (Vtx‘𝐺) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2322adantr 481 . . . . . . . 8 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
24233ad2ant1 1132 . . . . . . 7 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2524impcom 408 . . . . . 6 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
26253adant3 1131 . . . . 5 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
27 simprl 768 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐴 ∈ Word (Vtx‘𝐺))
28 simpll 764 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐵 ∈ Word (Vtx‘𝐺))
29 simprr 770 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐴 ≠ ∅)
30 ccatval1lsw 14289 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴))
3127, 28, 29, 30syl3anc 1370 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴))
3231adantr 481 . . . . . . . . . . . . . 14 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴))
333nn0cnd 12295 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈ ℂ)
34 npcan1 11400 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐴) ∈ ℂ → (((♯‘𝐴) − 1) + 1) = (♯‘𝐴))
3533, 34syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Word (Vtx‘𝐺) → (((♯‘𝐴) − 1) + 1) = (♯‘𝐴))
3635ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → (((♯‘𝐴) − 1) + 1) = (♯‘𝐴))
3736fveq2d 6778 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = ((𝐴 ++ 𝐵)‘(♯‘𝐴)))
38 simplr 766 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐵 ≠ ∅)
39 ccatval21sw 14290 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))
4027, 28, 38, 39syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))
4137, 40eqtrd 2778 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0))
4241adantr 481 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0))
43 simpr 485 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝐴‘0) = (𝐵‘0))
4442, 43eqtr4d 2781 . . . . . . . . . . . . . 14 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐴‘0))
4532, 44preq12d 4677 . . . . . . . . . . . . 13 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} = {(lastS‘𝐴), (𝐴‘0)})
4645eleq1d 2823 . . . . . . . . . . . 12 ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ({((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)))
4746exbiri 808 . . . . . . . . . . 11 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴‘0) = (𝐵‘0) → ({(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
4847com23 86 . . . . . . . . . 10 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ({(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
4948expimpd 454 . . . . . . . . 9 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
50493ad2ant1 1132 . . . . . . . 8 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
5150com12 32 . . . . . . 7 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
52513adant2 1130 . . . . . 6 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))))
53523imp 1110 . . . . 5 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))
54 ralunb 4125 . . . . . 6 (∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55 ovex 7308 . . . . . . . 8 ((♯‘𝐴) − 1) ∈ V
56 fveq2 6774 . . . . . . . . . 10 (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)))
57 fvoveq1 7298 . . . . . . . . . 10 (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)))
5856, 57preq12d 4677 . . . . . . . . 9 (𝑖 = ((♯‘𝐴) − 1) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))})
5958eleq1d 2823 . . . . . . . 8 (𝑖 = ((♯‘𝐴) − 1) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))
6055, 59ralsn 4617 . . . . . . 7 (∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))
6160anbi2i 623 . . . . . 6 ((∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))
6254, 61bitri 274 . . . . 5 (∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))
6326, 53, 62sylanbrc 583 . . . 4 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
64 0z 12330 . . . . . . . 8 0 ∈ ℤ
65 lennncl 14237 . . . . . . . . 9 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈ ℕ)
66 0p1e1 12095 . . . . . . . . . . . 12 (0 + 1) = 1
6766fveq2i 6777 . . . . . . . . . . 11 (ℤ‘(0 + 1)) = (ℤ‘1)
6867eleq2i 2830 . . . . . . . . . 10 ((♯‘𝐴) ∈ (ℤ‘(0 + 1)) ↔ (♯‘𝐴) ∈ (ℤ‘1))
69 elnnuz 12622 . . . . . . . . . 10 ((♯‘𝐴) ∈ ℕ ↔ (♯‘𝐴) ∈ (ℤ‘1))
7068, 69bitr4i 277 . . . . . . . . 9 ((♯‘𝐴) ∈ (ℤ‘(0 + 1)) ↔ (♯‘𝐴) ∈ ℕ)
7165, 70sylibr 233 . . . . . . . 8 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈ (ℤ‘(0 + 1)))
72 fzosplitsnm1 13462 . . . . . . . 8 ((0 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ‘(0 + 1))) → (0..^(♯‘𝐴)) = ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}))
7364, 71, 72sylancr 587 . . . . . . 7 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (0..^(♯‘𝐴)) = ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}))
7473raleqdv 3348 . . . . . 6 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
75743ad2ant1 1132 . . . . 5 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
76753ad2ant1 1132 . . . 4 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7763, 76mpbird 256 . . 3 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
78 lencl 14236 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈ ℕ0)
7978nn0zd 12424 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈ ℤ)
80 peano2zm 12363 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐵) ∈ ℤ → ((♯‘𝐵) − 1) ∈ ℤ)
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐵) − 1) ∈ ℤ)
8281ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐵) − 1) ∈ ℤ)
8382adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐵) − 1) ∈ ℤ)
8483anim1ci 616 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧ ((♯‘𝐵) − 1) ∈ ℤ))
85 fzosubel3 13448 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧ ((♯‘𝐵) − 1) ∈ ℤ) → (𝑖 − (♯‘𝐴)) ∈ (0..^((♯‘𝐵) − 1)))
86 fveq2 6774 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵𝑗) = (𝐵‘(𝑖 − (♯‘𝐴))))
87 fvoveq1 7298 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵‘(𝑗 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1)))
8886, 87preq12d 4677 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑖 − (♯‘𝐴)) → {(𝐵𝑗), (𝐵‘(𝑗 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))})
8988eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑖 − (♯‘𝐴)) → ({(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺)))
9089rspcv 3557 . . . . . . . . . . . . . . . 16 ((𝑖 − (♯‘𝐴)) ∈ (0..^((♯‘𝐵) − 1)) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺)))
9184, 85, 903syl 18 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺)))
92 simp-4l 780 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝐴 ∈ Word (Vtx‘𝐺))
93 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → 𝐵 ∈ Word (Vtx‘𝐺))
9493ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝐵 ∈ Word (Vtx‘𝐺))
953adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈ ℕ0)
9678adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈ ℕ0)
97 nn0addcl 12268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ0)
9897nn0zd 12424 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
9995, 96, 98syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
100 1nn0 12249 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℕ0
101 eluzmn 12589 . . . . . . . . . . . . . . . . . . . . . . 23 ((((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ ∧ 1 ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘(((♯‘𝐴) + (♯‘𝐵)) − 1)))
10299, 100, 101sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘(((♯‘𝐴) + (♯‘𝐵)) − 1)))
10333ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐴) ∈ ℂ)
10478nn0cnd 12295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈ ℂ)
105104ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐵) ∈ ℂ)
106 1cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → 1 ∈ ℂ)
107103, 105, 106addsubassd 11352 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (((♯‘𝐴) + (♯‘𝐵)) − 1) = ((♯‘𝐴) + ((♯‘𝐵) − 1)))
108107fveq2d 6778 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (ℤ‘(((♯‘𝐴) + (♯‘𝐵)) − 1)) = (ℤ‘((♯‘𝐴) + ((♯‘𝐵) − 1))))
109102, 108eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘((♯‘𝐴) + ((♯‘𝐵) − 1))))
110 fzoss2 13415 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘((♯‘𝐴) + ((♯‘𝐵) − 1))) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
111109, 110syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
112111adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
113112sselda 3921 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
114 ccatval2 14283 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴))))
11592, 94, 113, 114syl3anc 1370 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴))))
116107oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) = ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))
117116eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
118117adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
119 eluzmn 12589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((♯‘𝐴) ∈ ℤ ∧ 1 ∈ ℕ0) → (♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)))
1204, 100, 119sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)))
121120ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)))
122 fzoss1 13414 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)))
123121, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)))
124123sseld 3920 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1))))
125118, 124sylbird 259 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1))))
126125imp 407 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)))
1274adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈ ℤ)
12879adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈ ℤ)
129 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝐴) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → (♯‘𝐴) ∈ ℤ)
130 zaddcl 12360 . . . . . . . . . . . . . . . . . . . . . . . 24 (((♯‘𝐴) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
131129, 130jca 512 . . . . . . . . . . . . . . . . . . . . . . 23 (((♯‘𝐴) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ))
132127, 128, 131syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ))
133132adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ))
134 elfzoelz 13387 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈ ℤ)
135 1zzd 12351 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 1 ∈ ℤ)
136134, 135jca 512 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → (𝑖 ∈ ℤ ∧ 1 ∈ ℤ))
137 elfzomelpfzo 13491 . . . . . . . . . . . . . . . . . . . . 21 ((((♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) ∧ (𝑖 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
138133, 136, 137syl2an 596 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
139126, 138mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
140 ccatval2 14283 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴))))
14192, 94, 139, 140syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴))))
142134zcnd 12427 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈ ℂ)
143142adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ℂ)
144 1cnd 10970 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 1 ∈ ℂ)
145103ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (♯‘𝐴) ∈ ℂ)
146143, 144, 145addsubd 11353 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝑖 + 1) − (♯‘𝐴)) = ((𝑖 − (♯‘𝐴)) + 1))
147146fveq2d 6778 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝐵‘((𝑖 + 1) − (♯‘𝐴))) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1)))
148141, 147eqtrd 2778 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1)))
149115, 148preq12d 4677 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))})
150149eleq1d 2823 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺)))
15191, 150sylibrd 258 . . . . . . . . . . . . . 14 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
152151impancom 452 . . . . . . . . . . . . 13 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
153152ralrimiv 3102 . . . . . . . . . . . 12 (((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
154153exp31 420 . . . . . . . . . . 11 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((𝐴‘0) = (𝐵‘0) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
155154expcom 414 . . . . . . . . . 10 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
156155com23 86 . . . . . . . . 9 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
157156com24 95 . . . . . . . 8 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
158157imp 407 . . . . . . 7 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1591583adant3 1131 . . . . . 6 (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
160159com12 32 . . . . 5 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1611603ad2ant1 1132 . . . 4 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1621613imp 1110 . . 3 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
163 ralunb 4125 . . 3 (∀𝑖 ∈ ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
16477, 162, 163sylanbrc 583 . 2 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
165 ccatlen 14278 . . . . . . . . . . 11 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵)))
166165oveq1d 7290 . . . . . . . . . 10 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1))
167166ad2ant2r 744 . . . . . . . . 9 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1))
168167, 107eqtrd 2778 . . . . . . . 8 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘(𝐴 ++ 𝐵)) − 1) = ((♯‘𝐴) + ((♯‘𝐵) − 1)))
169168oveq2d 7291 . . . . . . 7 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (0..^((♯‘(𝐴 ++ 𝐵)) − 1)) = (0..^((♯‘𝐴) + ((♯‘𝐵) − 1))))
170 elnn0uz 12623 . . . . . . . . . 10 ((♯‘𝐴) ∈ ℕ0 ↔ (♯‘𝐴) ∈ (ℤ‘0))
1713, 170sylib 217 . . . . . . . . 9 (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈ (ℤ‘0))
172171adantr 481 . . . . . . . 8 ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈ (ℤ‘0))
173 lennncl 14237 . . . . . . . . 9 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈ ℕ)
174 nnm1nn0 12274 . . . . . . . . 9 ((♯‘𝐵) ∈ ℕ → ((♯‘𝐵) − 1) ∈ ℕ0)
175173, 174syl 17 . . . . . . . 8 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((♯‘𝐵) − 1) ∈ ℕ0)
176 fzoun 13424 . . . . . . . 8 (((♯‘𝐴) ∈ (ℤ‘0) ∧ ((♯‘𝐵) − 1) ∈ ℕ0) → (0..^((♯‘𝐴) + ((♯‘𝐵) − 1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
177172, 175, 176syl2an 596 . . . . . . 7 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (0..^((♯‘𝐴) + ((♯‘𝐵) − 1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
178169, 177eqtrd 2778 . . . . . 6 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (0..^((♯‘(𝐴 ++ 𝐵)) − 1)) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
1791783ad2antr1 1187 . . . . 5 (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) → (0..^((♯‘(𝐴 ++ 𝐵)) − 1)) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
1801793ad2antl1 1184 . . . 4 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) → (0..^((♯‘(𝐴 ++ 𝐵)) − 1)) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
1811803adant3 1131 . . 3 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → (0..^((♯‘(𝐴 ++ 𝐵)) − 1)) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))))
182181raleqdv 3348 . 2 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → (∀𝑖 ∈ (0..^((♯‘(𝐴 ++ 𝐵)) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
183164, 182mpbird 256 1 ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝐴 ++ 𝐵)) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wne 2943  wral 3064  cun 3885  wss 3887  c0 4256  {csn 4561  {cpr 4563  cfv 6433  (class class class)co 7275  cc 10869  0cc0 10871  1c1 10872   + caddc 10874  cmin 11205  cn 11973  0cn0 12233  cz 12319  cuz 12582  ..^cfzo 13382  chash 14044  Word cword 14217  lastSclsw 14265   ++ cconcat 14273  Vtxcvtx 27366  Edgcedg 27417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383  df-hash 14045  df-word 14218  df-lsw 14266  df-concat 14274
This theorem is referenced by:  clwwlkccat  28354
  Copyright terms: Public domain W3C validator