This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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