Metamath Proof Explorer

Theorem evl1fval

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1fval.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1fval.q ⊢ 𝑄 = ( 1o eval 𝑅 )
evl1fval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion evl1fval 𝑂 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 )

Proof

Step Hyp Ref Expression
1 evl1fval.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2 evl1fval.q ⊢ 𝑄 = ( 1o eval 𝑅 )
3 evl1fval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 fvexd ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
5 id ⊢ ( 𝑏 = ( Base ‘ 𝑟 ) → 𝑏 = ( Base ‘ 𝑟 ) )
6 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7 6 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8 5 7 sylan9eqr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → 𝑏 = 𝐵 )
9 8 oveq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑏 ↑m 1o ) = ( 𝐵 ↑m 1o ) )
10 8 9 oveq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) = ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) )
11 8 mpteq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
12 11 coeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
13 10 12 mpteq12dv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
14 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → 𝑟 = 𝑅 )
15 14 oveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 1o eval 𝑟 ) = ( 1o eval 𝑅 ) )
16 15 2 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 1o eval 𝑟 ) = 𝑄 )
17 13 16 coeq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
18 4 17 csbied ⊢ ( 𝑟 = 𝑅 → ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
19 df-evl1 ⊢ eval1 = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) )
20 ovex ⊢ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ∈ V
21 20 mptex ⊢ ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ V
22 2 ovexi ⊢ 𝑄 ∈ V
23 21 22 coex ⊢ ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) ∈ V
24 18 19 23 fvmpt ⊢ ( 𝑅 ∈ V → ( eval1 ‘ 𝑅 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
25 1 24 syl5eq ⊢ ( 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
26 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( eval1 ‘ 𝑅 ) = ∅ )
27 1 26 syl5eq ⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
28 co02 ⊢ ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) = ∅
29 27 28 eqtr4di ⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) )
30 df-evl ⊢ eval = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) )
31 30 reldmmpo ⊢ Rel dom eval
32 31 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( 1o eval 𝑅 ) = ∅ )
33 2 32 syl5eq ⊢ ( ¬ 𝑅 ∈ V → 𝑄 = ∅ )
34 33 coeq2d ⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) )
35 29 34 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
36 25 35 pm2.61i ⊢ 𝑂 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 )