eupth2lem3lem3fi - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > eupth2lem3lem3fi		GIF version

Theorem eupth2lem3lem3fi 16482

Description: Lemma for eupth2lem3fi 16488. If a loop {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 21-Feb-2021.)

**Hypotheses**
Ref	Expression
trlsegvdeg.v	⊢ 𝑉 = (Vtx‘𝐺)
trlsegvdeg.i	⊢ 𝐼 = (iEdg‘𝐺)
trlsegvdeg.f	⊢ (𝜑 → Fun 𝐼)
trlsegvdeg.n	⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))
trlsegvdeg.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
trlsegvdeg.w	⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
trlsegvdeg.vx	⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)
trlsegvdeg.vy	⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)
trlsegvdeg.vz	⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)
trlsegvdeg.ix	⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
trlsegvdeg.iy	⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})
trlsegvdeg.iz	⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))
trlsegvdegfi.g	⊢ (𝜑 → 𝐺 ∈ UPGraph)
trlsegvdegfi.v	⊢ (𝜑 → 𝑉 ∈ Fin)
eupth2lem3.o	⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))
eupth2lem3lem3.e	⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))

**Assertion**
Ref	Expression
eupth2lem3lem3fi	⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))

Distinct variable groups: 𝑥,𝑈 𝑥,𝑉 𝑥,𝑋 Allowed substitution hints: 𝜑(𝑥) 𝑃(𝑥) 𝐹(𝑥) 𝐺(𝑥) 𝐼(𝑥) 𝑁(𝑥) 𝑌(𝑥) 𝑍(𝑥)

**Proof of Theorem eupth2lem3lem3fi**
Step	Hyp	Ref	Expression
1		trlsegvdeg.u	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
2		fveq2 5672	. . . . . . . 8 ⊢ (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈))
3	2	breq2d 4123	. . . . . . 7 ⊢ (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
4	3	notbid 673	. . . . . 6 ⊢ (𝑥 = 𝑈 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
5	4	elrab3 2976	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
6	1, 5	syl 14	. . . 4 ⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
7		eupth2lem3.o	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))
8	7	eleq2d 2304	. . . 4 ⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
9	6, 8	bitr3d 190	. . 3 ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
10	9	adantr 276	. 2 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
11		2z 9607	. . . . . 6 ⊢ 2 ∈ ℤ
12	11	a1i 9	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∈ ℤ)
13		trlsegvdeg.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
14		trlsegvdeg.i	. . . . . . . 8 ⊢ 𝐼 = (iEdg‘𝐺)
15		trlsegvdeg.f	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐼)
16		trlsegvdeg.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))
17		trlsegvdeg.w	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
18		trlsegvdeg.vx	. . . . . . . 8 ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)
19		trlsegvdeg.vy	. . . . . . . 8 ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)
20		trlsegvdeg.vz	. . . . . . . 8 ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)
21		trlsegvdeg.ix	. . . . . . . 8 ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
22		trlsegvdeg.iy	. . . . . . . 8 ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})
23		trlsegvdeg.iz	. . . . . . . 8 ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))
24		trlsegvdegfi.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ UPGraph)
25		trlsegvdegfi.v	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ Fin)
26	13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23, 24, 25	eupth2lem3lem1fi 16480	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ₀)
27	26	nn0zd 9701	. . . . . 6 ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ)
28	27	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ)
29	13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 23, 24, 25	eupth2lem3lem2fi 16481	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ₀)
30	29	nn0zd 9701	. . . . . 6 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ)
31	30	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ)
32		z2even 12604	. . . . . . 7 ⊢ 2 ∥ 2
33	19	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (Vtx‘𝑌) = 𝑉)
34	14	trlf1 16400	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼)
35		f1f 5575	. . . . . . . . . . 11 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
36	17, 34, 35	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
37	36, 16	ffvelcdmd 5815	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑁) ∈ dom 𝐼)
38	37	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (𝐹‘𝑁) ∈ dom 𝐼)
39	1	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 𝑈 ∈ 𝑉)
40	22	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})
41		eupth2lem3lem3.e	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))
42	41	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))
43		ifptru 998	. . . . . . . . . . . . . 14 ⊢ ((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}))
44	43	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))) ↔ (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}))
45	42, 44	mpbid 147	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)})
46		sneq 3702	. . . . . . . . . . . . 13 ⊢ ((𝑃‘𝑁) = 𝑈 → {(𝑃‘𝑁)} = {𝑈})
47	46	eqcoms 2237	. . . . . . . . . . . 12 ⊢ (𝑈 = (𝑃‘𝑁) → {(𝑃‘𝑁)} = {𝑈})
48	45, 47	sylan9eq 2287	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (𝐼‘(𝐹‘𝑁)) = {𝑈})
49	48	opeq2d 3892	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → ⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩ = ⟨(𝐹‘𝑁), {𝑈}⟩)
50	49	sneqd 3704	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩} = {⟨(𝐹‘𝑁), {𝑈}⟩})
51	40, 50	eqtrd 2267	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), {𝑈}⟩})
52	25	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 𝑉 ∈ Fin)
53	33, 38, 39, 51, 52	1loopgrvd2fi 16317	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 2)
54	32, 53	breqtrrid 4149	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈))
55		z0even 12601	. . . . . . 7 ⊢ 2 ∥ 0
56	19	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (Vtx‘𝑌) = 𝑉)
57	37	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝐹‘𝑁) ∈ dom 𝐼)
58	13, 14, 15, 16, 1, 17	trlsegvdeglem1 16472	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
59	58	simpld 112	. . . . . . . . 9 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
60	59	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝑃‘𝑁) ∈ 𝑉)
61	22	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})
62	45	opeq2d 3892	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩ = ⟨(𝐹‘𝑁), {(𝑃‘𝑁)}⟩)
63	62	sneqd 3704	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩} = {⟨(𝐹‘𝑁), {(𝑃‘𝑁)}⟩})
64	61, 63	eqtrd 2267	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), {(𝑃‘𝑁)}⟩})
65	64	adantr 276	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), {(𝑃‘𝑁)}⟩})
66	25	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 𝑉 ∈ Fin)
67	1	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 𝑈 ∈ 𝑉)
68	67	anim1i 340	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝑈 ∈ 𝑉 ∧ 𝑈 ≠ (𝑃‘𝑁)))
69		eldifsn 3822	. . . . . . . . 9 ⊢ (𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)}) ↔ (𝑈 ∈ 𝑉 ∧ 𝑈 ≠ (𝑃‘𝑁)))
70	68, 69	sylibr 134	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)}))
71	56, 57, 60, 65, 66, 70	1loopgrvd0fi 16318	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 0)
72	55, 71	breqtrrid 4149	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈))
73	25	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 𝑉 ∈ Fin)
74		trliswlk 16398	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
75	13	wlkp 16346	. . . . . . . . . . 11 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
76	17, 74, 75	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
77		elfzofz 10501	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (0..^(♯‘𝐹)) → 𝑁 ∈ (0...(♯‘𝐹)))
78	16, 77	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝐹)))
79	76, 78	ffvelcdmd 5815	. . . . . . . . 9 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
80	79	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃‘𝑁) ∈ 𝑉)
81		fidceq 7126	. . . . . . . 8 ⊢ ((𝑉 ∈ Fin ∧ 𝑈 ∈ 𝑉 ∧ (𝑃‘𝑁) ∈ 𝑉) → DECID 𝑈 = (𝑃‘𝑁))
82	73, 67, 80, 81	syl3anc 1274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → DECID 𝑈 = (𝑃‘𝑁))
83		dcne 2425	. . . . . . 7 ⊢ (DECID 𝑈 = (𝑃‘𝑁) ↔ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 ≠ (𝑃‘𝑁)))
84	82, 83	sylib 122	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 = (𝑃‘𝑁) ∨ 𝑈 ≠ (𝑃‘𝑁)))
85	54, 72, 84	mpjaodan 806	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈))
86		dvdsadd2b 12530	. . . . 5 ⊢ ((2 ∈ ℤ ∧ ((VtxDeg‘𝑋)‘𝑈) ∈ ℤ ∧ (((VtxDeg‘𝑌)‘𝑈) ∈ ℤ ∧ 2 ∥ ((VtxDeg‘𝑌)‘𝑈))) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈))))
87	12, 28, 31, 85, 86	syl112anc 1278	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈))))
88	29	nn0cnd 9557	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℂ)
89	26	nn0cnd 9557	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℂ)
90	88, 89	addcomd 8426	. . . . . 6 ⊢ (𝜑 → (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))
91	90	breq2d 4123	. . . . 5 ⊢ (𝜑 → (2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))))
92	91	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))))
93	87, 92	bitrd 188	. . 3 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))))
94	93	notbid 673	. 2 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ ¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))))
95		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃‘𝑁) = (𝑃‘(𝑁 + 1)))
96	95	eqeq2d 2246	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑃‘0) = (𝑃‘𝑁) ↔ (𝑃‘0) = (𝑃‘(𝑁 + 1))))
97	95	preq2d 3777	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃‘𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))})
98	96, 97	ifbieq2d 3649	. . 3 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) = if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))
99	98	eleq2d 2304	. 2 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
100	10, 94, 99	3bitr3d 218	1 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 DECID wdc 842 if-wif 986 = wceq 1398 ∈ wcel 2205 ≠ wne 2414 {crab 2526 ∖ cdif 3210 ⊆ wss 3213 ∅c0 3510 ifcif 3622 {csn 3691 {cpr 3692 ⟨cop 3694 class class class wbr 4111 dom cdm 4751 ↾ cres 4753 “ cima 4754 Fun wfun 5348 ⟶wf 5350 –1-1→wf1 5351 ‘cfv 5354 (class class class)co 6052 Fincfn 6977 0cc0 8129 1c1 8130 + caddc 8132 2c2 9290 ℤcz 9579 ...cfz 10345 ..^cfzo 10480 ♯chash 11142 ∥ cdvds 12477 Vtxcvtx 16024 iEdgciedg 16025 UPGraphcupgr 16103 VtxDegcvtxdg 16298 Walkscwlks 16329 Trailsctrls 16392

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712 ax-cnex 8220 ax-resscn 8221 ax-1cn 8222 ax-1re 8223 ax-icn 8224 ax-addcl 8225 ax-addrcl 8226 ax-mulcl 8227 ax-addcom 8229 ax-mulcom 8230 ax-addass 8231 ax-mulass 8232 ax-distr 8233 ax-i2m1 8234 ax-0lt1 8235 ax-1rid 8236 ax-0id 8237 ax-rnegex 8238 ax-cnre 8240 ax-pre-ltirr 8241 ax-pre-ltwlin 8242 ax-pre-lttrn 8243 ax-pre-apti 8244 ax-pre-ltadd 8245

This theorem depends on definitions: df-bi 117 df-dc 843 df-ifp 987 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rab 2531 df-v 2817 df-sbc 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-if 3623 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-id 4416 df-iord 4489 df-on 4491 df-ilim 4492 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-riota 6005 df-ov 6055 df-oprab 6056 df-mpo 6057 df-1st 6336 df-2nd 6337 df-recs 6538 df-frec 6624 df-1o 6649 df-2o 6650 df-er 6769 df-map 6886 df-en 6978 df-dom 6979 df-fin 6980 df-pnf 8312 df-mnf 8313 df-xr 8314 df-ltxr 8315 df-le 8316 df-sub 8448 df-neg 8449 df-inn 9240 df-2 9298 df-3 9299 df-4 9300 df-5 9301 df-6 9302 df-7 9303 df-8 9304 df-9 9305 df-n0 9499 df-z 9580 df-dec 9713 df-uz 9857 df-xadd 10109 df-fz 10346 df-fzo 10481 df-ihash 11143 df-word 11229 df-dvds 12478 df-ndx 13232 df-slot 13233 df-base 13235 df-edgf 16017 df-vtx 16026 df-iedg 16027 df-edg 16070 df-uhgrm 16081 df-ushgrm 16082 df-upgren 16105 df-uspgren 16167 df-subgr 16266 df-vtxdg 16299 df-wlks 16330 df-trls 16393

This theorem is referenced by: eupth2lem3lem7fi 16486

W3C validator