uspgrn2crct

Description: In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 3-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

		Ref	Expression
	Assertion	uspgrn2crct	$⊢ (G \in USHGraph \land F Circuits (G) P) \to \|F\| \neq 2$

Proof

Step	Hyp	Ref	Expression
1		crctprop	$⊢ F Circuits (G) P \to (F Trails (G) P \land P (0) = P (\|F\|))$
2		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
3		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5		eqid	$⊢ iEdg (G) = iEdg (G)$
6	4 5	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
7		preq2	$⊢ P (2) = P (0) \to \{P (1), P (2)\} = \{P (1), P (0)\}$
8		prcom	$⊢ \{P (1), P (0)\} = \{P (0), P (1)\}$
9	7 8	eqtrdi	$⊢ P (2) = P (0) \to \{P (1), P (2)\} = \{P (0), P (1)\}$
10	9	eqcoms	$⊢ P (0) = P (2) \to \{P (1), P (2)\} = \{P (0), P (1)\}$
11	10	eqeq2d	$⊢ P (0) = P (2) \to (iEdg (G) (F (1)) = \{P (1), P (2)\} \leftrightarrow iEdg (G) (F (1)) = \{P (0), P (1)\})$
12	11	anbi2d	$⊢ P (0) = P (2) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (0), P (1)\}))$
13	12	ad2antrr	$⊢ ((P (0) = P (2) \land (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph))) \land F \in Word dom iEdg (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (0), P (1)\}))$
14		eqtr3	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (0), P (1)\}) \to iEdg (G) (F (0)) = iEdg (G) (F (1))$
15	4 5	uspgrf	$⊢ G \in USHGraph \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
16	15	adantl	$⊢ (Fun F^{-1} \land G \in USHGraph) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
17	16	adantl	$⊢ (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
18	17	adantr	$⊢ ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \land F \in Word dom iEdg (G)) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| \leq 2\}$
19		df-f1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom iEdg (G) \land Fun F^{-1})$
20	19	simplbi2	$⊢ F : (0 ..^\|F\|) ⟶ dom iEdg (G) \to (Fun F^{-1} \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G))$
21		wrdf	$⊢ F \in Word dom iEdg (G) \to F : (0 ..^\|F\|) ⟶ dom iEdg (G)$
22	20 21	syl11	$⊢ Fun F^{-1} \to (F \in Word dom iEdg (G) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G))$
23	22	adantr	$⊢ (Fun F^{-1} \land G \in USHGraph) \to (F \in Word dom iEdg (G) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G))$
24	23	adantl	$⊢ (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to (F \in Word dom iEdg (G) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G))$
25	24	imp	$⊢ ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \land F \in Word dom iEdg (G)) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G)$
26		2nn	$⊢ 2 \in ℕ$
27		lbfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow 2 \in ℕ$
28	26 27	mpbir	$⊢ 0 \in (0 ..^2)$
29		1nn0	$⊢ 1 \in ℕ_{0}$
30		1lt2	$⊢ 1 < 2$
31		elfzo0	$⊢ 1 \in (0 ..^2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ \land 1 < 2)$
32	29 26 30 31	mpbir3an	$⊢ 1 \in (0 ..^2)$
33	28 32	pm3.2i	$⊢ (0 \in (0 ..^2) \land 1 \in (0 ..^2))$
34		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
35	34	eleq2d	$⊢ \|F\| = 2 \to (0 \in (0 ..^\|F\|) \leftrightarrow 0 \in (0 ..^2))$
36	34	eleq2d	$⊢ \|F\| = 2 \to (1 \in (0 ..^\|F\|) \leftrightarrow 1 \in (0 ..^2))$
37	35 36	anbi12d	$⊢ \|F\| = 2 \to ((0 \in (0 ..^\|F\|) \land 1 \in (0 ..^\|F\|)) \leftrightarrow (0 \in (0 ..^2) \land 1 \in (0 ..^2)))$
38	33 37	mpbiri	$⊢ \|F\| = 2 \to (0 \in (0 ..^\|F\|) \land 1 \in (0 ..^\|F\|))$
39	38	ad2antrr	$⊢ ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \land F \in Word dom iEdg (G)) \to (0 \in (0 ..^\|F\|) \land 1 \in (0 ..^\|F\|))$
40		f1cofveqaeq	$⊢ ((iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \| \|x\| \leq 2\} \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G)) \land (0 \in (0 ..^\|F\|) \land 1 \in (0 ..^\|F\|))) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to 0 = 1)$
41	18 25 39 40	syl21anc	$⊢ ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \land F \in Word dom iEdg (G)) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to 0 = 1)$
42		0ne1	$⊢ 0 \neq 1$
43		eqneqall	$⊢ 0 = 1 \to (0 \neq 1 \to P (0) \neq P (2))$
44	41 42 43	syl6mpi	$⊢ ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \land F \in Word dom iEdg (G)) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to P (0) \neq P (2))$
45	44	adantll	$⊢ ((P (0) = P (2) \land (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph))) \land F \in Word dom iEdg (G)) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to P (0) \neq P (2))$
46	14 45	syl5	$⊢ ((P (0) = P (2) \land (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph))) \land F \in Word dom iEdg (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (0), P (1)\}) \to P (0) \neq P (2))$
47	13 46	sylbid	$⊢ ((P (0) = P (2) \land (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph))) \land F \in Word dom iEdg (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))$
48	47	expimpd	$⊢ (P (0) = P (2) \land (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph))) \to ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2))$
49	48	ex	$⊢ P (0) = P (2) \to ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2)))$
50		2a1	$⊢ P (0) \neq P (2) \to ((\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2)))$
51	49 50	pm2.61ine	$⊢ (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2))$
52		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
53	34 52	eqtrdi	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = \{0, 1\}$
54	53	raleqdv	$⊢ \|F\| = 2 \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow \forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
55		2wlklem	$⊢ \forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})$
56	54 55	bitrdi	$⊢ \|F\| = 2 \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}))$
57	56	anbi2d	$⊢ \|F\| = 2 \to ((F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \leftrightarrow (F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})))$
58		fveq2	$⊢ \|F\| = 2 \to P (\|F\|) = P (2)$
59	58	neeq2d	$⊢ \|F\| = 2 \to (P (0) \neq P (\|F\|) \leftrightarrow P (0) \neq P (2))$
60	57 59	imbi12d	$⊢ \|F\| = 2 \to (((F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to P (0) \neq P (\|F\|)) \leftrightarrow ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2)))$
61	60	adantr	$⊢ (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to (((F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to P (0) \neq P (\|F\|)) \leftrightarrow ((F \in Word dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2)))$
62	51 61	mpbird	$⊢ (\|F\| = 2 \land (Fun F^{-1} \land G \in USHGraph)) \to ((F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to P (0) \neq P (\|F\|))$
63	62	ex	$⊢ \|F\| = 2 \to ((Fun F^{-1} \land G \in USHGraph) \to ((F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to P (0) \neq P (\|F\|)))$
64	63	com13	$⊢ (F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to ((Fun F^{-1} \land G \in USHGraph) \to (\|F\| = 2 \to P (0) \neq P (\|F\|)))$
65	64	expd	$⊢ (F \in Word dom iEdg (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to (Fun F^{-1} \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|))))$
66	65	3adant2	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to (Fun F^{-1} \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|))))$
67	6 66	syl6bi	$⊢ G \in UPGraph \to (F Walks (G) P \to (Fun F^{-1} \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|)))))$
68	67	impd	$⊢ G \in UPGraph \to ((F Walks (G) P \land Fun F^{-1}) \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|))))$
69	68	com23	$⊢ G \in UPGraph \to (G \in USHGraph \to ((F Walks (G) P \land Fun F^{-1}) \to (\|F\| = 2 \to P (0) \neq P (\|F\|))))$
70	3 69	mpcom	$⊢ G \in USHGraph \to ((F Walks (G) P \land Fun F^{-1}) \to (\|F\| = 2 \to P (0) \neq P (\|F\|)))$
71	70	com12	$⊢ (F Walks (G) P \land Fun F^{-1}) \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|)))$
72	2 71	sylbi	$⊢ F Trails (G) P \to (G \in USHGraph \to (\|F\| = 2 \to P (0) \neq P (\|F\|)))$
73	72	imp	$⊢ (F Trails (G) P \land G \in USHGraph) \to (\|F\| = 2 \to P (0) \neq P (\|F\|))$
74	73	necon2d	$⊢ (F Trails (G) P \land G \in USHGraph) \to (P (0) = P (\|F\|) \to \|F\| \neq 2)$
75	74	impancom	$⊢ (F Trails (G) P \land P (0) = P (\|F\|)) \to (G \in USHGraph \to \|F\| \neq 2)$
76	1 75	syl	$⊢ F Circuits (G) P \to (G \in USHGraph \to \|F\| \neq 2)$
77	76	impcom	$⊢ (G \in USHGraph \land F Circuits (G) P) \to \|F\| \neq 2$

Metamath Proof Explorer

Theorem uspgrn2crct

Proof