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 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
axlowdimlem14.2 
|- R = ( { <. ( J + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( J + 1 ) } ) X. { 0 } ) )
Assertion axlowdimlem14 
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( Q = R -> I = J ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem14.1 
 |-  Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
2 axlowdimlem14.2 
 |-  R = ( { <. ( J + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( J + 1 ) } ) X. { 0 } ) )
3 1 axlowdimlem10 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) )
4 elee 
 |-  ( N e. NN -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) )
5 4 adantr 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) )
6 3 5 mpbid 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q : ( 1 ... N ) --> RR )
7 6 ffnd 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q Fn ( 1 ... N ) )
8 2 axlowdimlem10 
 |-  ( ( N e. NN /\ J e. ( 1 ... ( N - 1 ) ) ) -> R e. ( EE ` N ) )
9 elee 
 |-  ( N e. NN -> ( R e. ( EE ` N ) <-> R : ( 1 ... N ) --> RR ) )
10 9 adantr 
 |-  ( ( N e. NN /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( R e. ( EE ` N ) <-> R : ( 1 ... N ) --> RR ) )
11 8 10 mpbid 
 |-  ( ( N e. NN /\ J e. ( 1 ... ( N - 1 ) ) ) -> R : ( 1 ... N ) --> RR )
12 11 ffnd 
 |-  ( ( N e. NN /\ J e. ( 1 ... ( N - 1 ) ) ) -> R Fn ( 1 ... N ) )
13 eqfnfv 
 |-  ( ( Q Fn ( 1 ... N ) /\ R Fn ( 1 ... N ) ) -> ( Q = R <-> A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) ) )
14 7 12 13 syl2an 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) /\ ( N e. NN /\ J e. ( 1 ... ( N - 1 ) ) ) ) -> ( Q = R <-> A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) ) )
15 14 3impdi 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( Q = R <-> A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) ) )
16 fznatpl1 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )
17 16 3adant3 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )
18 ax-1ne0 
 |-  1 =/= 0
19 18 a1i 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) /\ I =/= J ) -> 1 =/= 0 )
20 1 axlowdimlem11 
 |-  ( Q ` ( I + 1 ) ) = 1
21 20 a1i 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) /\ I =/= J ) -> ( Q ` ( I + 1 ) ) = 1 )
22 elfzelz 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. ZZ )
23 22 zcnd 
 |-  ( I e. ( 1 ... ( N - 1 ) ) -> I e. CC )
24 elfzelz 
 |-  ( J e. ( 1 ... ( N - 1 ) ) -> J e. ZZ )
25 24 zcnd 
 |-  ( J e. ( 1 ... ( N - 1 ) ) -> J e. CC )
26 ax-1cn 
 |-  1 e. CC
27 addcan2 
 |-  ( ( I e. CC /\ J e. CC /\ 1 e. CC ) -> ( ( I + 1 ) = ( J + 1 ) <-> I = J ) )
28 26 27 mp3an3 
 |-  ( ( I e. CC /\ J e. CC ) -> ( ( I + 1 ) = ( J + 1 ) <-> I = J ) )
29 23 25 28 syl2an 
 |-  ( ( I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( ( I + 1 ) = ( J + 1 ) <-> I = J ) )
30 29 3adant1 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( ( I + 1 ) = ( J + 1 ) <-> I = J ) )
31 30 necon3bid 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( ( I + 1 ) =/= ( J + 1 ) <-> I =/= J ) )
32 31 biimpar 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) /\ I =/= J ) -> ( I + 1 ) =/= ( J + 1 ) )
33 2 axlowdimlem12 
 |-  ( ( ( I + 1 ) e. ( 1 ... N ) /\ ( I + 1 ) =/= ( J + 1 ) ) -> ( R ` ( I + 1 ) ) = 0 )
34 17 32 33 syl2an2r 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) /\ I =/= J ) -> ( R ` ( I + 1 ) ) = 0 )
35 19 21 34 3netr4d 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 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 ) e. ( 1 ... N ) /\ ( Q ` ( I + 1 ) ) =/= ( R ` ( I + 1 ) ) ) -> E. i e. ( 1 ... N ) -. ( Q ` i ) = ( R ` i ) )
42 17 35 41 syl2an2r 
 |-  ( ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) /\ I =/= J ) -> E. i e. ( 1 ... N ) -. ( Q ` i ) = ( R ` i ) )
43 42 ex 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( I =/= J -> E. i e. ( 1 ... N ) -. ( Q ` i ) = ( R ` i ) ) )
44 df-ne 
 |-  ( I =/= J <-> -. I = J )
45 rexnal 
 |-  ( E. i e. ( 1 ... N ) -. ( Q ` i ) = ( R ` i ) <-> -. A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) )
46 43 44 45 3imtr3g 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( -. I = J -> -. A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) ) )
47 46 con4d 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( Q ` i ) = ( R ` i ) -> I = J ) )
48 15 47 sylbid 
 |-  ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) /\ J e. ( 1 ... ( N - 1 ) ) ) -> ( Q = R -> I = J ) )