Metamath Proof Explorer


Theorem 2cycld

Description: Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023)

Ref Expression
Hypotheses 2cycld.1 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2cycld.2 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2cycld.3 ( 𝜑 → ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) )
2cycld.4 ( 𝜑 → ( 𝐴𝐵𝐵𝐶 ) )
2cycld.5 ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼𝐾 ) ) )
2cycld.6 𝑉 = ( Vtx ‘ 𝐺 )
2cycld.7 𝐼 = ( iEdg ‘ 𝐺 )
2cycld.8 ( 𝜑𝐽𝐾 )
2cycld.9 ( 𝜑𝐴 = 𝐶 )
Assertion 2cycld ( 𝜑𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )

Proof

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 ‘ 𝐺 ) 𝑃 )