# Metamath Proof Explorer

## 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 𝐵 ) )