Metamath Proof Explorer


Theorem etransclem1

Description: H is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem1.x φ X
etransclem1.p φ P
etransclem1.h H = j 0 M x X x j if j = 0 P 1 P
etransclem1.j φ J 0 M
Assertion etransclem1 φ H J : X

Proof

Step Hyp Ref Expression
1 etransclem1.x φ X
2 etransclem1.p φ P
3 etransclem1.h H = j 0 M x X x j if j = 0 P 1 P
4 etransclem1.j φ J 0 M
5 1 sselda φ x X x
6 4 elfzelzd φ J
7 6 zcnd φ J
8 7 adantr φ x X J
9 5 8 subcld φ x X x J
10 nnm1nn0 P P 1 0
11 2 10 syl φ P 1 0
12 2 nnnn0d φ P 0
13 11 12 ifcld φ if J = 0 P 1 P 0
14 13 adantr φ x X if J = 0 P 1 P 0
15 9 14 expcld φ x X x J if J = 0 P 1 P
16 eqid x X x J if J = 0 P 1 P = x X x J if J = 0 P 1 P
17 15 16 fmptd φ x X x J if J = 0 P 1 P : X
18 oveq2 j = n x j = x n
19 eqeq1 j = n j = 0 n = 0
20 19 ifbid j = n if j = 0 P 1 P = if n = 0 P 1 P
21 18 20 oveq12d j = n x j if j = 0 P 1 P = x n if n = 0 P 1 P
22 21 mpteq2dv j = n x X x j if j = 0 P 1 P = x X x n if n = 0 P 1 P
23 22 cbvmptv j 0 M x X x j if j = 0 P 1 P = n 0 M x X x n if n = 0 P 1 P
24 3 23 eqtri H = n 0 M x X x n if n = 0 P 1 P
25 oveq2 n = J x n = x J
26 eqeq1 n = J n = 0 J = 0
27 26 ifbid n = J if n = 0 P 1 P = if J = 0 P 1 P
28 25 27 oveq12d n = J x n if n = 0 P 1 P = x J if J = 0 P 1 P
29 28 mpteq2dv n = J x X x n if n = 0 P 1 P = x X x J if J = 0 P 1 P
30 cnex V
31 30 ssex X X V
32 mptexg X V x X x J if J = 0 P 1 P V
33 1 31 32 3syl φ x X x J if J = 0 P 1 P V
34 24 29 4 33 fvmptd3 φ H J = x X x J if J = 0 P 1 P
35 34 feq1d φ H J : X x X x J if J = 0 P 1 P : X
36 17 35 mpbird φ H J : X