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 14571 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℕ0) |
| 4 | 3 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℤ) |
| 5 | | fzossrbm1 13728 |
. . . . . . . . . . . . . . . . . . . 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 3983 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈
(0..^(♯‘𝐴))) |
| 9 | | ccatval1 14615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
| 10 | 1, 2, 8, 9 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
| 11 | 4 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘𝐴) ∈ ℤ) |
| 12 | | elfzom1elp1fzo 13771 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝐴)
∈ ℤ ∧ 𝑖
∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴))) |
| 13 | 11, 12 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈
(0..^(♯‘𝐴))) |
| 14 | | ccatval1 14615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1))) |
| 15 | 1, 2, 13, 14 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐴‘(𝑖 + 1))) |
| 16 | 10, 15 | preq12d 4741 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐴‘𝑖), (𝐴‘(𝑖 + 1))}) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 18 | 17 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 19 | 18 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 20 | 19 | impancom 451 |
. . . . . . . . . . 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 480 |
. . . . . . . 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 407 |
. . . . . 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 14622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
| 31 | 27, 28, 29, 30 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴)) |
| 33 | 3 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
ℂ) |
| 34 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . 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 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = ((𝐴 ++ 𝐵)‘(♯‘𝐴))) |
| 38 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → 𝐵 ≠ ∅) |
| 39 | | ccatval21sw 14623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) |
| 40 | 27, 28, 38, 39 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) |
| 41 | 37, 40 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0)) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐵‘0)) |
| 43 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝐴‘0) = (𝐵‘0)) |
| 44 | 42, 43 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1)) = (𝐴‘0)) |
| 45 | 32, 44 | preq12d 4741 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ (𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} = {(lastS‘𝐴), (𝐴‘0)}) |
| 46 | 45 | eleq1d 2826 |
. . . . . . . . . . . 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 453 |
. . . . . . . . 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 1111 |
. . . . 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 4197 |
. . . . . 6
⊢
(∀𝑖 ∈
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 55 | | ovex 7464 |
. . . . . . . 8
⊢
((♯‘𝐴)
− 1) ∈ V |
| 56 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1))) |
| 57 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑖 = ((♯‘𝐴) − 1) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))) |
| 58 | 56, 57 | preq12d 4741 |
. . . . . . . . 9
⊢ (𝑖 = ((♯‘𝐴) − 1) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))}) |
| 59 | 58 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝐴) − 1) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
| 60 | 55, 59 | ralsn 4681 |
. . . . . . 7
⊢
(∀𝑖 ∈
{((♯‘𝐴) −
1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺)) |
| 61 | 60 | anbi2i 623 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝐴) − 1)} {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
| 62 | 54, 61 | bitri 275 |
. . . . 5
⊢
(∀𝑖 ∈
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)}){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)), ((𝐴 ++ 𝐵)‘(((♯‘𝐴) − 1) + 1))} ∈ (Edg‘𝐺))) |
| 63 | 26, 53, 62 | sylanbrc 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 12624 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
| 65 | | lennncl 14572 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℕ) |
| 66 | | 0p1e1 12388 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
| 67 | 66 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
| 68 | 67 | eleq2i 2833 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ (ℤ≥‘(0 + 1)) ↔ (♯‘𝐴) ∈
(ℤ≥‘1)) |
| 69 | | elnnuz 12922 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ ℕ ↔ (♯‘𝐴) ∈
(ℤ≥‘1)) |
| 70 | 68, 69 | bitr4i 278 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ (ℤ≥‘(0 + 1)) ↔ (♯‘𝐴) ∈
ℕ) |
| 71 | 65, 70 | sylibr 234 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
(ℤ≥‘(0 + 1))) |
| 72 | | fzosplitsnm1 13779 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ≥‘(0 +
1))) → (0..^(♯‘𝐴)) = ((0..^((♯‘𝐴) − 1)) ∪ {((♯‘𝐴) − 1)})) |
| 73 | 64, 71, 72 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) →
(0..^(♯‘𝐴)) =
((0..^((♯‘𝐴)
− 1)) ∪ {((♯‘𝐴) − 1)})) |
| 74 | 73 | raleqdv 3326 |
. . . . . 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 257 |
. . 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 14571 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℕ0) |
| 79 | 78 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℤ) |
| 80 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐵)
∈ ℤ → ((♯‘𝐵) − 1) ∈
ℤ) |
| 81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐵) − 1) ∈
ℤ) |
| 82 | 81 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐵) − 1) ∈
ℤ) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐵) − 1) ∈
ℤ) |
| 84 | 83 | anim1ci 616 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧ ((♯‘𝐵) − 1) ∈
ℤ)) |
| 85 | | fzosubel3 13765 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ∧
((♯‘𝐵) −
1) ∈ ℤ) → (𝑖 − (♯‘𝐴)) ∈ (0..^((♯‘𝐵) − 1))) |
| 86 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵‘𝑗) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
| 87 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → (𝐵‘(𝑗 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
| 88 | 86, 87 | preq12d 4741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → {(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))}) |
| 89 | 88 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑖 − (♯‘𝐴)) → ({(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
| 90 | 89 | rspcv 3618 |
. . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℕ0) |
| 96 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℕ0) |
| 97 | | nn0addcl 12561 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℕ0) |
| 98 | 97 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 99 | 95, 96, 98 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
ℤ) |
| 100 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℕ0 |
| 101 | | eluzmn 12885 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((♯‘𝐴)
+ (♯‘𝐵)) ∈
ℤ ∧ 1 ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
| 102 | 99, 100, 101 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
| 103 | 33 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐴) ∈
ℂ) |
| 104 | 78 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (♯‘𝐵) ∈
ℂ) |
| 105 | 104 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (♯‘𝐵) ∈
ℂ) |
| 106 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → 1 ∈
ℂ) |
| 107 | 103, 105,
106 | addsubassd 11640 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(((♯‘𝐴) +
(♯‘𝐵)) −
1) = ((♯‘𝐴) +
((♯‘𝐵) −
1))) |
| 108 | 107 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(ℤ≥‘(((♯‘𝐴) + (♯‘𝐵)) − 1)) =
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
| 109 | 102, 108 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) + (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
| 110 | | fzoss2 13727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝐴)
+ (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + ((♯‘𝐵) − 1))) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) ⊆
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 113 | 112 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 114 | | ccatval2 14616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
| 115 | 92, 94, 113, 114 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
| 116 | 107 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) =
((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) |
| 117 | 116 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
| 118 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
| 119 | | eluzmn 12885 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝐴)
∈ ℤ ∧ 1 ∈ ℕ0) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
| 120 | 4, 100, 119 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
| 121 | 120 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
| 122 | | fzoss1 13726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝐴)
∈ (ℤ≥‘((♯‘𝐴) − 1)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1))) |
| 123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ⊆
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1))) |
| 124 | 123 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) −
1)))) |
| 125 | 118, 124 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) −
1)))) |
| 126 | 125 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1))) |
| 127 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℤ) |
| 128 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℤ) |
| 129 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
(♯‘𝐴) ∈
ℤ) |
| 130 | | zaddcl 12657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 131 | 129, 130 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) ∈
ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)) |
| 132 | 127, 128,
131 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) → ((♯‘𝐴) ∈ ℤ ∧
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ)) |
| 134 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈
ℤ) |
| 135 | | 1zzd 12648 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 1 ∈
ℤ) |
| 136 | 134, 135 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → (𝑖 ∈ ℤ ∧ 1 ∈
ℤ)) |
| 137 | | elfzomelpfzo 13810 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((♯‘𝐴)
∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) ∧ (𝑖 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑖 ∈
(((♯‘𝐴) −
1)..^(((♯‘𝐴) +
(♯‘𝐵)) −
1)) ↔ (𝑖 + 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
| 138 | 133, 136,
137 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 ∈ (((♯‘𝐴) − 1)..^(((♯‘𝐴) + (♯‘𝐵)) − 1)) ↔ (𝑖 + 1) ∈
((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
| 139 | 126, 138 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 140 | | ccatval2 14616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴)))) |
| 141 | 92, 94, 139, 140 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 + 1) − (♯‘𝐴)))) |
| 142 | 134 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → 𝑖 ∈
ℂ) |
| 143 | 142 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → 𝑖 ∈ ℂ) |
| 144 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . 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 11641 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝑖 + 1) − (♯‘𝐴)) = ((𝑖 − (♯‘𝐴)) + 1)) |
| 147 | 146 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (𝐵‘((𝑖 + 1) − (♯‘𝐴))) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
| 148 | 141, 147 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ((𝐴 ++ 𝐵)‘(𝑖 + 1)) = (𝐵‘((𝑖 − (♯‘𝐴)) + 1))) |
| 149 | 115, 148 | preq12d 4741 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} = {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))}) |
| 150 | 149 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → ({((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘(𝑖 − (♯‘𝐴))), (𝐵‘((𝑖 − (♯‘𝐴)) + 1))} ∈ (Edg‘𝐺))) |
| 151 | 91, 150 | sylibrd 259 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))) → (∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 152 | 151 | impancom 451 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → (𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))) → {((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 153 | 152 | ralrimiv 3145 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ Word
(Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) ∧ (𝐴‘0) = (𝐵‘0)) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 154 | 153 | exp31 419 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) → ((𝐴‘0) = (𝐵‘0) → (∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
| 155 | 154 | expcom 413 |
. . . . . . . . . 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 406 |
. . . . . . 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 1111 |
. . 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 4197 |
. . 3
⊢
(∀𝑖 ∈
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1)))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(♯‘𝐴)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 164 | 77, 162, 163 | sylanbrc 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 14613 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
| 166 | 165 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ∈ Word (Vtx‘𝐺)) → ((♯‘(𝐴 ++ 𝐵)) − 1) = (((♯‘𝐴) + (♯‘𝐵)) − 1)) |
| 167 | 166 | ad2ant2r 747 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
((♯‘(𝐴 ++ 𝐵)) − 1) =
(((♯‘𝐴) +
(♯‘𝐵)) −
1)) |
| 168 | 167, 107 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
((♯‘(𝐴 ++ 𝐵)) − 1) =
((♯‘𝐴) +
((♯‘𝐵) −
1))) |
| 169 | 168 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
(0..^((♯‘𝐴) +
((♯‘𝐵) −
1)))) |
| 170 | | elnn0uz 12923 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ0 ↔ (♯‘𝐴) ∈
(ℤ≥‘0)) |
| 171 | 3, 170 | sylib 218 |
. . . . . . . 8
⊢ (𝐴 ∈ Word (Vtx‘𝐺) → (♯‘𝐴) ∈
(ℤ≥‘0)) |
| 172 | 171 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
(ℤ≥‘0)) |
| 173 | | lennncl 14572 |
. . . . . . . 8
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℕ) |
| 174 | | nnm1nn0 12567 |
. . . . . . . 8
⊢
((♯‘𝐵)
∈ ℕ → ((♯‘𝐵) − 1) ∈
ℕ0) |
| 175 | 173, 174 | syl 17 |
. . . . . . 7
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) → ((♯‘𝐵) − 1) ∈
ℕ0) |
| 176 | | fzoun 13736 |
. . . . . . 7
⊢
(((♯‘𝐴)
∈ (ℤ≥‘0) ∧ ((♯‘𝐵) − 1) ∈ ℕ0)
→ (0..^((♯‘𝐴) + ((♯‘𝐵) − 1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) −
1))))) |
| 177 | 172, 175,
176 | syl2an 596 |
. . . . . 6
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘𝐴) +
((♯‘𝐵) −
1))) = ((0..^(♯‘𝐴)) ∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
| 178 | 169, 177 | eqtrd 2777 |
. . . . 5
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅)) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
| 179 | 178 | 3ad2antr1 1189 |
. . . 4
⊢ (((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈
(0..^((♯‘𝐵)
− 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺))) →
(0..^((♯‘(𝐴 ++
𝐵)) − 1)) =
((0..^(♯‘𝐴))
∪ ((♯‘𝐴)..^((♯‘𝐴) + ((♯‘𝐵) − 1))))) |
| 180 | 179 | 3ad2antl1 1186 |
. . 3
⊢ ((((𝐴 ∈ 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 |
. 2
⊢ ((((𝐴 ∈ 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 | 164, 181 | raleqtrrdv 3330 |
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‘𝐺)) |