Metamath Proof Explorer

Theorem lp1cycl

Description: A loop (which is an edge at index J ) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Hypothesis	lppthon.i	$⊢ I = iEdg (G)$
	Assertion	lp1cycl	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ J ”⟩ Cycles (G) ⟨“ A A ”⟩$

Proof

Step	Hyp	Ref	Expression
1		lppthon.i	$⊢ I = iEdg (G)$
2	1	lppthon	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ J ”⟩ (A PathsOn (G) A) ⟨“ A A ”⟩$
3		pthonispth	$⊢ ⟨“ J ”⟩ (A PathsOn (G) A) ⟨“ A A ”⟩ \to ⟨“ J ”⟩ Paths (G) ⟨“ A A ”⟩$
4	2 3	syl	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ J ”⟩ Paths (G) ⟨“ A A ”⟩$
5	1	lpvtx	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to A \in Vtx (G)$
6		s2fv1	$⊢ A \in Vtx (G) \to ⟨“ A A ”⟩ (1) = A$
7		s1len	$⊢ \|⟨“ J ”⟩\| = 1$
8	7	fveq2i	$⊢ ⟨“ A A ”⟩ (\|⟨“ J ”⟩\|) = ⟨“ A A ”⟩ (1)$
9	8	a1i	$⊢ A \in Vtx (G) \to ⟨“ A A ”⟩ (\|⟨“ J ”⟩\|) = ⟨“ A A ”⟩ (1)$
10		s2fv0	$⊢ A \in Vtx (G) \to ⟨“ A A ”⟩ (0) = A$
11	6 9 10	3eqtr4rd	$⊢ A \in Vtx (G) \to ⟨“ A A ”⟩ (0) = ⟨“ A A ”⟩ (\|⟨“ J ”⟩\|)$
12	5 11	syl	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ A A ”⟩ (0) = ⟨“ A A ”⟩ (\|⟨“ J ”⟩\|)$
13		iscycl	$⊢ ⟨“ J ”⟩ Cycles (G) ⟨“ A A ”⟩ \leftrightarrow (⟨“ J ”⟩ Paths (G) ⟨“ A A ”⟩ \land ⟨“ A A ”⟩ (0) = ⟨“ A A ”⟩ (\|⟨“ J ”⟩\|))$
14	4 12 13	sylanbrc	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to ⟨“ J ”⟩ Cycles (G) ⟨“ A A ”⟩$