Metamath Proof Explorer

Theorem slotsdifunifndx

Description: The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT . (Contributed by AV, 10-Nov-2024)

Ref Expression
Assertion slotsdifunifndx 
|- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1nn 
 |-  1 e. NN
3 3nn0 
 |-  3 e. NN0
4 2nn0 
 |-  2 e. NN0
5 2lt10 
 |-  2 < ; 1 0
6 2 3 4 5 declti 
 |-  2 < ; 1 3
7 1 6 ltneii 
 |-  2 =/= ; 1 3
8 plusgndx 
 |-  ( +g ` ndx ) = 2
9 unifndx 
 |-  ( UnifSet ` ndx ) = ; 1 3
10 8 9 neeq12i 
 |-  ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) <-> 2 =/= ; 1 3 )
11 7 10 mpbir 
 |-  ( +g ` ndx ) =/= ( UnifSet ` ndx )
12 3re 
 |-  3 e. RR
13 3lt10 
 |-  3 < ; 1 0
14 2 3 3 13 declti 
 |-  3 < ; 1 3
15 12 14 ltneii 
 |-  3 =/= ; 1 3
16 mulrndx 
 |-  ( .r ` ndx ) = 3
17 16 9 neeq12i 
 |-  ( ( .r ` ndx ) =/= ( UnifSet ` ndx ) <-> 3 =/= ; 1 3 )
18 15 17 mpbir 
 |-  ( .r ` ndx ) =/= ( UnifSet ` ndx )
19 4re 
 |-  4 e. RR
20 4nn0 
 |-  4 e. NN0
21 4lt10 
 |-  4 < ; 1 0
22 2 3 20 21 declti 
 |-  4 < ; 1 3
23 19 22 ltneii 
 |-  4 =/= ; 1 3
24 starvndx 
 |-  ( *r ` ndx ) = 4
25 24 9 neeq12i 
 |-  ( ( *r ` ndx ) =/= ( UnifSet ` ndx ) <-> 4 =/= ; 1 3 )
26 23 25 mpbir 
 |-  ( *r ` ndx ) =/= ( UnifSet ` ndx )
27 11 18 26 3pm3.2i 
 |-  ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) )
28 10re 
 |-  ; 1 0 e. RR
29 1nn0 
 |-  1 e. NN0
30 0nn0 
 |-  0 e. NN0
31 3nn 
 |-  3 e. NN
32 3pos 
 |-  0 < 3
33 29 30 31 32 declt 
 |-  ; 1 0 < ; 1 3
34 28 33 ltneii 
 |-  ; 1 0 =/= ; 1 3
35 plendx 
 |-  ( le ` ndx ) = ; 1 0
36 35 9 neeq12i 
 |-  ( ( le ` ndx ) =/= ( UnifSet ` ndx ) <-> ; 1 0 =/= ; 1 3 )
37 34 36 mpbir 
 |-  ( le ` ndx ) =/= ( UnifSet ` ndx )
38 2nn 
 |-  2 e. NN
39 29 38 decnncl 
 |-  ; 1 2 e. NN
40 39 nnrei 
 |-  ; 1 2 e. RR
41 2lt3 
 |-  2 < 3
42 29 4 31 41 declt 
 |-  ; 1 2 < ; 1 3
43 40 42 ltneii 
 |-  ; 1 2 =/= ; 1 3
44 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
45 44 9 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( UnifSet ` ndx ) <-> ; 1 2 =/= ; 1 3 )
46 43 45 mpbir 
 |-  ( dist ` ndx ) =/= ( UnifSet ` ndx )
47 37 46 pm3.2i 
 |-  ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) )
48 27 47 pm3.2i 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )