Theorem edginwlk

Description: The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021) (Revised by AV, 9-Dec-2021)

	Ref	Expression
Hypotheses	edginwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	edginwlk.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	edginwlk	⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		edginwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		edginwlk.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		simp1	⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → Fun 𝐼 )
4		wrdsymbcl	⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 )
5	4	3adant1	⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 )
6		fvelrn	⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝐾 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ ran 𝐼 )
7	3 5 6	syl2anc	⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ ran 𝐼 )
8		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
9	1	eqcomi	⊢ ( iEdg ‘ 𝐺 ) = 𝐼
10	9	rneqi	⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
11	2 8 10	3eqtri	⊢ 𝐸 = ran 𝐼
12	7 11	eleqtrrdi	⊢ ( ( Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝐾 ) ) ∈ 𝐸 )