Metamath Proof Explorer


Theorem coe1mul2lem1

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Assertion coe1mul2lem1 A 0 X 0 1 𝑜 X f 1 𝑜 × A X 0 A

Proof

Step Hyp Ref Expression
1 1on 1 𝑜 On
2 1 a1i A 0 X 0 1 𝑜 1 𝑜 On
3 fvexd A 0 X 0 1 𝑜 a 1 𝑜 X V
4 simpll A 0 X 0 1 𝑜 a 1 𝑜 A 0
5 df1o2 1 𝑜 =
6 nn0ex 0 V
7 0ex V
8 5 6 7 mapsnconst X 0 1 𝑜 X = 1 𝑜 × X
9 8 adantl A 0 X 0 1 𝑜 X = 1 𝑜 × X
10 fconstmpt 1 𝑜 × X = a 1 𝑜 X
11 9 10 eqtrdi A 0 X 0 1 𝑜 X = a 1 𝑜 X
12 fconstmpt 1 𝑜 × A = a 1 𝑜 A
13 12 a1i A 0 X 0 1 𝑜 1 𝑜 × A = a 1 𝑜 A
14 2 3 4 11 13 ofrfval2 A 0 X 0 1 𝑜 X f 1 𝑜 × A a 1 𝑜 X A
15 1n0 1 𝑜
16 r19.3rzv 1 𝑜 X A a 1 𝑜 X A
17 15 16 mp1i A 0 X 0 1 𝑜 X A a 1 𝑜 X A
18 elmapi X 0 1 𝑜 X : 1 𝑜 0
19 0lt1o 1 𝑜
20 ffvelrn X : 1 𝑜 0 1 𝑜 X 0
21 18 19 20 sylancl X 0 1 𝑜 X 0
22 21 adantl A 0 X 0 1 𝑜 X 0
23 22 biantrurd A 0 X 0 1 𝑜 X A X 0 X A
24 fznn0 A 0 X 0 A X 0 X A
25 24 adantr A 0 X 0 1 𝑜 X 0 A X 0 X A
26 23 25 bitr4d A 0 X 0 1 𝑜 X A X 0 A
27 14 17 26 3bitr2d A 0 X 0 1 𝑜 X f 1 𝑜 × A X 0 A