Metamath Proof Explorer


Theorem 1pthdlem2

Description: Lemma 2 for 1pthd . (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021)

Ref Expression
Hypotheses 1wlkd.p
|- P = <" X Y ">
1wlkd.f
|- F = <" J ">
Assertion 1pthdlem2
|- ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/)

Proof

Step Hyp Ref Expression
1 1wlkd.p
 |-  P = <" X Y ">
2 1wlkd.f
 |-  F = <" J ">
3 2 fveq2i
 |-  ( # ` F ) = ( # ` <" J "> )
4 s1len
 |-  ( # ` <" J "> ) = 1
5 3 4 eqtri
 |-  ( # ` F ) = 1
6 5 oveq2i
 |-  ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 1 )
7 fzo0
 |-  ( 1 ..^ 1 ) = (/)
8 6 7 eqtri
 |-  ( 1 ..^ ( # ` F ) ) = (/)
9 8 imaeq2i
 |-  ( P " ( 1 ..^ ( # ` F ) ) ) = ( P " (/) )
10 9 ineq2i
 |-  ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) )
11 ima0
 |-  ( P " (/) ) = (/)
12 11 ineq2i
 |-  ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) ) = ( ( P " { 0 , ( # ` F ) } ) i^i (/) )
13 in0
 |-  ( ( P " { 0 , ( # ` F ) } ) i^i (/) ) = (/)
14 12 13 eqtri
 |-  ( ( P " { 0 , ( # ` F ) } ) i^i ( P " (/) ) ) = (/)
15 10 14 eqtri
 |-  ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/)