Step |
Hyp |
Ref |
Expression |
1 |
|
2cycld.1 |
⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 |
2 |
|
2cycld.2 |
⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 |
3 |
|
2cycld.3 |
⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) |
4 |
|
2cycld.4 |
⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) |
5 |
|
2cycld.5 |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) ) |
6 |
|
2cycld.6 |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
7 |
|
2cycld.7 |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
8 |
|
2cycld.8 |
⊢ ( 𝜑 → 𝐽 ≠ 𝐾 ) |
9 |
|
2cycld.9 |
⊢ ( 𝜑 → 𝐴 = 𝐶 ) |
10 |
1 2 3 4 5 6 7 8
|
2pthd |
⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
11 |
1
|
fveq1i |
⊢ ( 𝑃 ‘ 0 ) = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 0 ) |
12 |
|
s3fv0 |
⊢ ( 𝐴 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 0 ) = 𝐴 ) |
13 |
11 12
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝐴 ) |
14 |
13
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑃 ‘ 0 ) = 𝐴 ) |
15 |
14
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 = 𝐶 ) → ( 𝑃 ‘ 0 ) = 𝐴 ) |
16 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 ) |
17 |
2
|
fveq2i |
⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) |
18 |
|
s2len |
⊢ ( ♯ ‘ 〈“ 𝐽 𝐾 ”〉 ) = 2 |
19 |
17 18
|
eqtri |
⊢ ( ♯ ‘ 𝐹 ) = 2 |
20 |
1 19
|
fveq12i |
⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 2 ) |
21 |
|
s3fv2 |
⊢ ( 𝐶 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ‘ 2 ) = 𝐶 ) |
22 |
20 21
|
eqtr2id |
⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
23 |
22
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
24 |
23
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 = 𝐶 ) → 𝐶 = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
25 |
15 16 24
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 = 𝐶 ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
26 |
3 9 25
|
syl2anc |
⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
27 |
|
iscycl |
⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
28 |
10 26 27
|
sylanbrc |
⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) |