Metamath Proof Explorer


Theorem axlowdimlem14

Description: Lemma for axlowdim . Take two possible Q from axlowdimlem10 . They are the same iff their distinguished values are the same. (Contributed by Scott Fenton, 21-Apr-2013)

Ref Expression
Hypotheses axlowdimlem14.1 Q = I + 1 1 1 N I + 1 × 0
axlowdimlem14.2 R = J + 1 1 1 N J + 1 × 0
Assertion axlowdimlem14 N I 1 N 1 J 1 N 1 Q = R I = J

Proof

Step Hyp Ref Expression
1 axlowdimlem14.1 Q = I + 1 1 1 N I + 1 × 0
2 axlowdimlem14.2 R = J + 1 1 1 N J + 1 × 0
3 1 axlowdimlem10 N I 1 N 1 Q 𝔼 N
4 elee N Q 𝔼 N Q : 1 N
5 4 adantr N I 1 N 1 Q 𝔼 N Q : 1 N
6 3 5 mpbid N I 1 N 1 Q : 1 N
7 6 ffnd N I 1 N 1 Q Fn 1 N
8 2 axlowdimlem10 N J 1 N 1 R 𝔼 N
9 elee N R 𝔼 N R : 1 N
10 9 adantr N J 1 N 1 R 𝔼 N R : 1 N
11 8 10 mpbid N J 1 N 1 R : 1 N
12 11 ffnd N J 1 N 1 R Fn 1 N
13 eqfnfv Q Fn 1 N R Fn 1 N Q = R i 1 N Q i = R i
14 7 12 13 syl2an N I 1 N 1 N J 1 N 1 Q = R i 1 N Q i = R i
15 14 3impdi N I 1 N 1 J 1 N 1 Q = R i 1 N Q i = R i
16 fznatpl1 N I 1 N 1 I + 1 1 N
17 16 3adant3 N I 1 N 1 J 1 N 1 I + 1 1 N
18 ax-1ne0 1 0
19 18 a1i N I 1 N 1 J 1 N 1 I J 1 0
20 1 axlowdimlem11 Q I + 1 = 1
21 20 a1i N I 1 N 1 J 1 N 1 I J Q I + 1 = 1
22 elfzelz I 1 N 1 I
23 22 zcnd I 1 N 1 I
24 elfzelz J 1 N 1 J
25 24 zcnd J 1 N 1 J
26 ax-1cn 1
27 addcan2 I J 1 I + 1 = J + 1 I = J
28 26 27 mp3an3 I J I + 1 = J + 1 I = J
29 23 25 28 syl2an I 1 N 1 J 1 N 1 I + 1 = J + 1 I = J
30 29 3adant1 N I 1 N 1 J 1 N 1 I + 1 = J + 1 I = J
31 30 necon3bid N I 1 N 1 J 1 N 1 I + 1 J + 1 I J
32 31 biimpar N I 1 N 1 J 1 N 1 I J I + 1 J + 1
33 2 axlowdimlem12 I + 1 1 N I + 1 J + 1 R I + 1 = 0
34 17 32 33 syl2an2r N I 1 N 1 J 1 N 1 I J R I + 1 = 0
35 19 21 34 3netr4d N I 1 N 1 J 1 N 1 I J Q I + 1 R I + 1
36 df-ne Q i R i ¬ Q i = R i
37 fveq2 i = I + 1 Q i = Q I + 1
38 fveq2 i = I + 1 R i = R I + 1
39 37 38 neeq12d i = I + 1 Q i R i Q I + 1 R I + 1
40 36 39 bitr3id i = I + 1 ¬ Q i = R i Q I + 1 R I + 1
41 40 rspcev I + 1 1 N Q I + 1 R I + 1 i 1 N ¬ Q i = R i
42 17 35 41 syl2an2r N I 1 N 1 J 1 N 1 I J i 1 N ¬ Q i = R i
43 42 ex N I 1 N 1 J 1 N 1 I J i 1 N ¬ Q i = R i
44 df-ne I J ¬ I = J
45 rexnal i 1 N ¬ Q i = R i ¬ i 1 N Q i = R i
46 43 44 45 3imtr3g N I 1 N 1 J 1 N 1 ¬ I = J ¬ i 1 N Q i = R i
47 46 con4d N I 1 N 1 J 1 N 1 i 1 N Q i = R i I = J
48 15 47 sylbid N I 1 N 1 J 1 N 1 Q = R I = J