Proof of Theorem clwwlkccatlem
Step | Hyp | Ref
| Expression |
1 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐴 ∈ Word (Vtx‘𝐺)) |
2 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺)) |
3 | | lencl 13974 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℕ0) |
4 | 3 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℤ) |
5 | | fzossrbm1 13157 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐴)
∈ ℤ → (0..^((♯‘𝐴) − 1)) ⊆
(0..^(♯‘𝐴))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Word (Vtx‘𝐺) →
(0..^((♯‘𝐴)
− 1)) ⊆ (0..^(♯‘𝐴))) |
7 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (0..^((♯‘𝐴) − 1)) ⊆
(0..^(♯‘𝐴))) |
8 | 7 | sselda 3877 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈
(0..^(♯‘𝐴))) |
9 | | ccatval1 14019 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
10 | 1, 2, 8, 9 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
11 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘𝐴) ∈ ℤ) |
12 | | elfzom1elp1fzo 13195 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝐴)
∈ ℤ ∧ 𝑖
∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴))) |
13 | 11, 12 | sylan 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈
(0..^(♯‘𝐴))) |
14 | | ccatval1 14019 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1))) |
15 | 1, 2, 13, 14 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1))) |
16 | 10, 15 | preq12d 4632 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐴‘𝑖), (𝐴‘(𝑖 + 1))}) |
17 | 16 | eleq1d 2817 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
18 | 17 | biimprd 251 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
19 | 18 | ralimdva 3091 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
20 | 19 | impancom 455 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝐵 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
21 | 20 | 3adant3 1133 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (𝐵 ∈ Word (Vtx‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
22 | 21 | com12 32 |
. . . . . . . . 9
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
23 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | 23 | 3ad2ant1 1134 |
. . . . . . 7
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
25 | 24 | impcom 411 |
. . . . . 6
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
26 | 25 | 3adant3 1133 |
. . . . 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 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐴 ∈ Word (Vtx‘𝐺)) |
28 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
29 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐴 ≠ ∅) |
30 | | ccatval1lsw 14027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
31 | 27, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
32 | 31 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
33 | 3 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℂ) |
34 | | npcan1 11143 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐴)
∈ ℂ → (((♯‘𝐴) − 1) + 1) = (♯‘𝐴)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (((♯‘𝐴) − 1) + 1) =
(♯‘𝐴)) |
36 | 35 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) →
(((♯‘𝐴) −
1) + 1) = (♯‘𝐴)) |
37 | 36 | fveq2d 6678 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = ((𝐴 ++ 𝐵)‘(♯‘𝐴))) |
38 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐵 ≠ ∅) |
39 | | ccatval21sw 14028 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) |
40 | 27, 28, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) |
41 | 37, 40 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0)) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0)) |
43 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝐴‘0) = (𝐵‘0)) |
44 | 42, 43 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐴‘0)) |
45 | 32, 44 | preq12d 4632 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} = {(lastS‘𝐴), (𝐴‘0)}) |
46 | 45 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ({((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺))) |
47 | 46 | exbiri 811 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴‘0) = (𝐵‘0) → ({(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))) |
48 | 47 | com23 86 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ({(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))) |
49 | 48 | expimpd 457 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))) |
50 | 49 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))) |
51 | 50 | com12 32 |
. . . . . . 7
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)))) |
52 | 51 | 3adant2 1132 |
. . . . . 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‘𝐺)))) |
53 | 52 | 3imp 1112 |
. . . . 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 4081 |
. . . . . 6
⊢
(∀𝑖 ∈
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
55 | | ovex 7203 |
. . . . . . . 8
⊢
((♯‘𝐴)
− 1) ∈ V |
56 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1))) |
57 | | fvoveq1 7193 |
. . . . . . . . . 10
⊢ (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))) |
58 | 56, 57 | preq12d 4632 |
. . . . . . . . 9
⊢ (𝑖 = ((♯‘𝐴) − 1) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))}) |
59 | 58 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝐴) − 1) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
60 | 55, 59 | ralsn 4572 |
. . . . . . 7
⊢
(∀𝑖 ∈
{((♯‘𝐴) −
1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)) |
61 | 60 | anbi2i 626 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
62 | 54, 61 | bitri 278 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
63 | 26, 53, 62 | sylanbrc 586 |
. . . 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 12073 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
65 | | lennncl 13975 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℕ) |
66 | | 0p1e1 11838 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
67 | 66 | fveq2i 6677 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
68 | 67 | eleq2i 2824 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ (ℤ≥‘(0 + 1)) ↔ (♯‘𝐴) ∈
(ℤ≥‘1)) |
69 | | elnnuz 12364 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ ℕ ↔ (♯‘𝐴) ∈
(ℤ≥‘1)) |
70 | 68, 69 | bitr4i 281 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ (ℤ≥‘(0 + 1)) ↔ (♯‘𝐴) ∈
ℕ) |
71 | 65, 70 | sylibr 237 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
(ℤ≥‘(0 + 1))) |
72 | | fzosplitsnm1 13203 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ≥‘(0 +
1))) → (0..^(♯‘𝐴)) = ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)})) |
73 | 64, 71, 72 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) →
(0..^(♯‘𝐴)) =
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)})) |
74 | 73 | raleqdv 3316 |
. . . . . 6
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (∀𝑖 ∈
(0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪
{((♯‘𝐴) −
1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
75 | 74 | 3ad2ant1 1134 |
. . . . 5
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈
(0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝐴) − 1)) ∪
{((♯‘𝐴) −
1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
76 | 75 | 3ad2ant1 1134 |
. . . 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‘𝐺))) |
77 | 63, 76 | mpbird 260 |
. . 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 13974 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℕ0) |
79 | 78 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℤ) |
80 | | peano2zm 12106 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐵)
∈ ℤ → ((♯‘𝐵) − 1) ∈
ℤ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐵) − 1) ∈
ℤ) |
82 | 81 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐵) − 1) ∈
ℤ) |
83 | 82 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐵) − 1) ∈
ℤ) |
84 | 83 | anim1ci 619 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧ ((♯‘𝐵) − 1) ∈
ℤ)) |
85 | | fzosubel3 13189 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧
((♯‘𝐵) −
1) ∈ ℤ) → (𝑖 − (♯‘𝐴)) ∈ (0..^((♯‘𝐵) − 1))) |
86 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵‘𝑗) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
87 | | fvoveq1 7193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵‘(𝑗 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
88 | 86, 87 | preq12d 4632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → {(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))}) |
89 | 88 | eleq1d 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → ({(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
90 | 89 | rspcv 3521 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 − (♯‘𝐴)) ∈
(0..^((♯‘𝐵)
− 1)) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
91 | 84, 85, 90 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
92 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝐴 ∈ Word (Vtx‘𝐺)) |
93 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
94 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝐵 ∈ Word (Vtx‘𝐺)) |
95 | 3 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℕ0) |
96 | 78 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℕ0) |
97 | | nn0addcl 12011 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℕ0) |
98 | 97 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
99 | 95, 96, 98 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
ℤ) |
100 | | 1nn0 11992 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℕ0 |
101 | | eluzmn 12331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((♯‘𝐴)
+ (♯‘𝐵)) ∈
ℤ ∧ 1 ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
102 | 99, 100, 101 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
103 | 33 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐴) ∈
ℂ) |
104 | 78 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℂ) |
105 | 104 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐵) ∈
ℂ) |
106 | | 1cnd 10714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → 1 ∈
ℂ) |
107 | 103, 105,
106 | addsubassd 11095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(((♯‘𝐴) +
(♯‘𝐵)) −
1) = ((♯‘𝐴) +
((♯‘𝐵) −
1))) |
108 | 107 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1)) =
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
109 | 102, 108 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
110 | | fzoss2 13156 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝐴)
+ (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1))) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
112 | 111 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
113 | 112 | sselda 3877 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
114 | | ccatval2 14021 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
115 | 92, 94, 113, 114 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
116 | 107 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) =
((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
117 | 116 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
118 | 117 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
119 | | eluzmn 12331 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝐴)
∈ ℤ ∧ 1 ∈ ℕ0) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
120 | 4, 100, 119 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
121 | 120 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
122 | | fzoss1 13155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝐴)
∈ (ℤ≥‘((♯‘𝐴) − 1)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1))) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1))) |
124 | 123 | sseld 3876 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) −
1)))) |
125 | 118, 124 | sylbird 263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) −
1)))) |
126 | 125 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
127 | 4 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℤ) |
128 | 79 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℤ) |
129 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
(♯‘𝐴) ∈
ℤ) |
130 | | zaddcl 12103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
131 | 129, 130 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) ∈
ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)) |
132 | 127, 128,
131 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ)) |
133 | 132 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ)) |
134 | | elfzoelz 13129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈
ℤ) |
135 | | 1zzd 12094 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 1 ∈
ℤ) |
136 | 134, 135 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → (𝑖 ∈ ℤ ∧ 1 ∈
ℤ)) |
137 | | elfzomelpfzo 13232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((♯‘𝐴)
∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) ∧ (𝑖 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑖 ∈
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1)) ↔ (𝑖 + 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
138 | 133, 136,
137 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ (𝑖 + 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
139 | 126, 138 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
140 | | ccatval2 14021 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴)))) |
141 | 92, 94, 139, 140 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴)))) |
142 | 134 | zcnd 12169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈
ℂ) |
143 | 142 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ℂ) |
144 | | 1cnd 10714 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 1 ∈
ℂ) |
145 | 103 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (♯‘𝐴) ∈
ℂ) |
146 | 143, 144,
145 | addsubd 11096 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝑖 + 1) − (♯‘𝐴)) = ((𝑖 − (♯‘𝐴)) + 1)) |
147 | 146 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝐵‘((𝑖 + 1) − (♯‘𝐴))) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
148 | 141, 147 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
149 | 115, 148 | preq12d 4632 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))}) |
150 | 149 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
151 | 91, 150 | sylibrd 262 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
152 | 151 | impancom 455 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
153 | 152 | ralrimiv 3095 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
154 | 153 | exp31 423 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((𝐴‘0) = (𝐵‘0) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
155 | 154 | expcom 417 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
156 | 155 | com23 86 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
157 | 156 | com24 95 |
. . . . . . . 8
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))) |
158 | 157 | imp 410 |
. . . . . . 7
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
159 | 158 | 3adant3 1133 |
. . . . . 6
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
160 | 159 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
161 | 160 | 3ad2ant1 1134 |
. . . 4
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) → (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) → ((𝐴‘0) = (𝐵‘0) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
162 | 161 | 3imp 1112 |
. . 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 4081 |
. . 3
⊢
(∀𝑖 ∈
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
164 | 77, 162, 163 | sylanbrc 586 |
. 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 14016 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
166 | 165 | oveq1d 7185 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1)) |
167 | 166 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
((♯‘(𝐴 ++ 𝐵)) − 1) =
(((♯‘𝐴) +
(♯‘𝐵)) −
1)) |
168 | 167, 107 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
((♯‘(𝐴 ++ 𝐵)) − 1) =
((♯‘𝐴) +
((♯‘𝐵) −
1))) |
169 | 168 | oveq2d 7186 |
. . . . . . 7
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
(0..^((♯‘𝐴) +
((♯‘𝐵) −
1)))) |
170 | | elnn0uz 12365 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ ℕ0 ↔ (♯‘𝐴) ∈
(ℤ≥‘0)) |
171 | 3, 170 | sylib 221 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
(ℤ≥‘0)) |
172 | 171 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
(ℤ≥‘0)) |
173 | | lennncl 13975 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℕ) |
174 | | nnm1nn0 12017 |
. . . . . . . . 9
⊢
((♯‘𝐵)
∈ ℕ → ((♯‘𝐵) − 1) ∈
ℕ0) |
175 | 173, 174 | syl 17 |
. . . . . . . 8
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((♯‘𝐵) − 1) ∈
ℕ0) |
176 | | fzoun 13165 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ (ℤ≥‘0) ∧ ((♯‘𝐵) − 1) ∈ ℕ0)
→ (0..^((♯‘𝐴) + ((♯‘𝐵) − 1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) −
1))))) |
177 | 172, 175,
176 | syl2an 599 |
. . . . . . 7
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘𝐴) +
((♯‘𝐵) −
1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
178 | 169, 177 | eqtrd 2773 |
. . . . . 6
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
179 | 178 | 3ad2antr1 1189 |
. . . . 5
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
180 | 179 | 3ad2antl1 1186 |
. . . 4
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
181 | 180 | 3adant3 1133 |
. . 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))))) |
182 | 181 | raleqdv 3316 |
. 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‘𝐺))) |
183 | 164, 182 | mpbird 260 |
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‘𝐺)) |