Theorem evl1fval1lem

Description: Lemma for evl1fval1 . (Contributed by AV, 11-Sep-2019)

	Ref	Expression
Hypotheses	evl1fval1.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
	evl1fval1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	evl1fval1lem	⊢ ( 𝑅 ∈ 𝑉 → 𝑄 = ( 𝑅 evalSub1 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		evl1fval1.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2		evl1fval1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
4		eqid	⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
5	3 4 2	evl1fval	⊢ ( eval1 ‘ 𝑅 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) )
6	1	a1i	⊢ ( 𝑅 ∈ 𝑉 → 𝑄 = ( eval1 ‘ 𝑅 ) )
7	2	fvexi	⊢ 𝐵 ∈ V
8	7	pwid	⊢ 𝐵 ∈ 𝒫 𝐵
9		eqid	⊢ ( 𝑅 evalSub1 𝐵 ) = ( 𝑅 evalSub1 𝐵 )
10		eqid	⊢ ( 1o evalSub 𝑅 ) = ( 1o evalSub 𝑅 )
11	9 10 2	evls1fval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝒫 𝐵 ) → ( 𝑅 evalSub1 𝐵 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑅 ) ‘ 𝐵 ) ) )
12	8 11	mpan2	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 evalSub1 𝐵 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑅 ) ‘ 𝐵 ) ) )
13	4 2	evlval	⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
14	13	eqcomi	⊢ ( ( 1o evalSub 𝑅 ) ‘ 𝐵 ) = ( 1o eval 𝑅 )
15	14	coeq2i	⊢ ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑅 ) ‘ 𝐵 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) )
16	12 15	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 evalSub1 𝐵 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) )
17	5 6 16	3eqtr4a	⊢ ( 𝑅 ∈ 𝑉 → 𝑄 = ( 𝑅 evalSub1 𝐵 ) )