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 O = eval 1 R
evl1fval.q Q = 1 𝑜 eval R
evl1fval.b B = Base R
Assertion evl1fval O = x B B 1 𝑜 x y B 1 𝑜 × y Q

Proof

Step Hyp Ref Expression
1 evl1fval.o O = eval 1 R
2 evl1fval.q Q = 1 𝑜 eval R
3 evl1fval.b B = Base R
4 fvexd r = R Base r V
5 id b = Base r b = Base r
6 fveq2 r = R Base r = Base R
7 6 3 syl6eqr r = R Base r = B
8 5 7 sylan9eqr r = R b = Base r b = B
9 8 oveq1d r = R b = Base r b 1 𝑜 = B 1 𝑜
10 8 9 oveq12d r = R b = Base r b b 1 𝑜 = B B 1 𝑜
11 8 mpteq1d r = R b = Base r y b 1 𝑜 × y = y B 1 𝑜 × y
12 11 coeq2d r = R b = Base r x y b 1 𝑜 × y = x y B 1 𝑜 × y
13 10 12 mpteq12dv r = R b = Base r x b b 1 𝑜 x y b 1 𝑜 × y = x B B 1 𝑜 x y B 1 𝑜 × y
14 simpl r = R b = Base r r = R
15 14 oveq2d r = R b = Base r 1 𝑜 eval r = 1 𝑜 eval R
16 15 2 syl6eqr r = R b = Base r 1 𝑜 eval r = Q
17 13 16 coeq12d r = R b = Base r x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 eval r = x B B 1 𝑜 x y B 1 𝑜 × y Q
18 4 17 csbied r = R Base r / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 eval r = x B B 1 𝑜 x y B 1 𝑜 × y Q
19 df-evl1 eval 1 = r V Base r / b x b b 1 𝑜 x y b 1 𝑜 × y 1 𝑜 eval r
20 ovex B B 1 𝑜 V
21 20 mptex x B B 1 𝑜 x y B 1 𝑜 × y V
22 2 ovexi Q V
23 21 22 coex x B B 1 𝑜 x y B 1 𝑜 × y Q V
24 18 19 23 fvmpt R V eval 1 R = x B B 1 𝑜 x y B 1 𝑜 × y Q
25 1 24 syl5eq R V O = x B B 1 𝑜 x y B 1 𝑜 × y Q
26 fvprc ¬ R V eval 1 R =
27 1 26 syl5eq ¬ R V O =
28 co02 x B B 1 𝑜 x y B 1 𝑜 × y =
29 27 28 syl6eqr ¬ R V O = x B B 1 𝑜 x y B 1 𝑜 × y
30 df-evl eval = i V , r V i evalSub r Base r
31 30 reldmmpo Rel dom eval
32 31 ovprc2 ¬ R V 1 𝑜 eval R =
33 2 32 syl5eq ¬ R V Q =
34 33 coeq2d ¬ R V x B B 1 𝑜 x y B 1 𝑜 × y Q = x B B 1 𝑜 x y B 1 𝑜 × y
35 29 34 eqtr4d ¬ R V O = x B B 1 𝑜 x y B 1 𝑜 × y Q
36 25 35 pm2.61i O = x B B 1 𝑜 x y B 1 𝑜 × y Q