eupth2lem3lem3fi - Intuitionistic Logic Explorer

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

Theorem eupth2lem3lem3fi 16591

Description: Lemma for eupth2lem3fi 16597. 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 5675	. . . . . . . 8 ⊢ (𝑥 = 𝑈 → ((VtxDeg‘𝑋)‘𝑥) = ((VtxDeg‘𝑋)‘𝑈))
3	2	breq2d 4126	. . . . . . 7 ⊢ (𝑥 = 𝑈 → (2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
4	3	notbid 673	. . . . . 6 ⊢ (𝑥 = 𝑈 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈)))
5	4	elrab3 2977	. . . . 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 9622	. . . . . 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 16589	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ₀)
27	26	nn0zd 9716	. . . . . 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 16590	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ₀)
30	29	nn0zd 9716	. . . . . 6 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ)
31	30	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((VtxDeg‘𝑌)‘𝑈) ∈ ℤ)
32		z2even 12625	. . . . . . 7 ⊢ 2 ∥ 2
33	19	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (Vtx‘𝑌) = 𝑉)
34	14	trlf1 16509	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼)
35		f1f 5578	. . . . . . . . . . 11 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
36	17, 34, 35	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
37	36, 16	ffvelcdmd 5818	. . . . . . . . 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 3705	. . . . . . . . . . . . 13 ⊢ ((𝑃‘𝑁) = 𝑈 → {(𝑃‘𝑁)} = {𝑈})
47	46	eqcoms 2237	. . . . . . . . . . . 12 ⊢ (𝑈 = (𝑃‘𝑁) → {(𝑃‘𝑁)} = {𝑈})
48	45, 47	sylan9eq 2287	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (𝐼‘(𝐹‘𝑁)) = {𝑈})
49	48	opeq2d 3895	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → ⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩ = ⟨(𝐹‘𝑁), {𝑈}⟩)
50	49	sneqd 3707	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩} = {⟨(𝐹‘𝑁), {𝑈}⟩})
51	40, 50	eqtrd 2267	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), {𝑈}⟩})
52	25	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 𝑉 ∈ Fin)
53	33, 38, 39, 51, 52	1loopgrvd2fi 16426	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 2)
54	32, 53	breqtrrid 4152	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 = (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈))
55		z0even 12622	. . . . . . 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 16581	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
59	58	simpld 112	. . . . . . . . 9 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
60	59	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → (𝑃‘𝑁) ∈ 𝑉)
61	22	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})
62	45	opeq2d 3895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩ = ⟨(𝐹‘𝑁), {(𝑃‘𝑁)}⟩)
63	62	sneqd 3707	. . . . . . . . . 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 3825	. . . . . . . . 9 ⊢ (𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)}) ↔ (𝑈 ∈ 𝑉 ∧ 𝑈 ≠ (𝑃‘𝑁)))
70	68, 69	sylibr 134	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 𝑈 ∈ (𝑉 ∖ {(𝑃‘𝑁)}))
71	56, 57, 60, 65, 66, 70	1loopgrvd0fi 16427	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → ((VtxDeg‘𝑌)‘𝑈) = 0)
72	55, 71	breqtrrid 4152	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ 𝑈 ≠ (𝑃‘𝑁)) → 2 ∥ ((VtxDeg‘𝑌)‘𝑈))
73	25	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 𝑉 ∈ Fin)
74		trliswlk 16507	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
75	13	wlkp 16455	. . . . . . . . . . 11 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
76	17, 74, 75	3syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
77		elfzofz 10519	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (0..^(♯‘𝐹)) → 𝑁 ∈ (0...(♯‘𝐹)))
78	16, 77	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝐹)))
79	76, 78	ffvelcdmd 5818	. . . . . . . . 9 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
80	79	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃‘𝑁) ∈ 𝑉)
81		fidceq 7137	. . . . . . . 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 12551	. . . . 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 9572	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℂ)
89	26	nn0cnd 9572	. . . . . . 7 ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℂ)
90	88, 89	addcomd 8440	. . . . . 6 ⊢ (𝜑 → (((VtxDeg‘𝑌)‘𝑈) + ((VtxDeg‘𝑋)‘𝑈)) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))
91	90	breq2d 4126	. . . . 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 3780	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃‘𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))})
98	96, 97	ifbieq2d 3651	. . 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 3211 ⊆ wss 3214 ∅c0 3512 ifcif 3624 {csn 3694 {cpr 3695 ⟨cop 3697 class class class wbr 4114 dom cdm 4754 ↾ cres 4756 “ cima 4757 Fun wfun 5351 ⟶wf 5353 –1-1→wf1 5354 ‘cfv 5357 (class class class)co 6058 Fincfn 6988 0cc0 8143 1c1 8144 + caddc 8146 2c2 9305 ℤcz 9594 ...cfz 10361 ..^cfzo 10498 ♯chash 11163 ∥ cdvds 12498 Vtxcvtx 16133 iEdgciedg 16134 UPGraphcupgr 16212 VtxDegcvtxdg 16407 Walkscwlks 16438 Trailsctrls 16501

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 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259

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 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-frec 6635 df-1o 6660 df-2o 6661 df-er 6780 df-map 6897 df-en 6989 df-dom 6990 df-fin 6991 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-5 9316 df-6 9317 df-7 9318 df-8 9319 df-9 9320 df-n0 9514 df-z 9595 df-dec 9728 df-uz 9872 df-xadd 10125 df-fz 10362 df-fzo 10499 df-ihash 11164 df-word 11250 df-dvds 12499 df-ndx 13299 df-slot 13300 df-base 13302 df-edgf 16126 df-vtx 16135 df-iedg 16136 df-edg 16179 df-uhgrm 16190 df-ushgrm 16191 df-upgren 16214 df-uspgren 16276 df-subgr 16375 df-vtxdg 16408 df-wlks 16439 df-trls 16502

This theorem is referenced by: eupth2lem3lem7fi 16595

W3C validator