Metamath Proof Explorer


Theorem istrkgld

Description: Property of fulfilling the lower dimension N axiom. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses istrkg.p P = Base G
istrkg.d - ˙ = dist G
istrkg.i I = Itv G
Assertion istrkgld G V N 2 G Dim 𝒢 N f f : 1 ..^ N 1-1 P x P y P z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z

Proof

Step Hyp Ref Expression
1 istrkg.p P = Base G
2 istrkg.d - ˙ = dist G
3 istrkg.i I = Itv G
4 eqidd p = P d = - ˙ i = I f = f
5 eqidd p = P d = - ˙ i = I 1 ..^ n = 1 ..^ n
6 simp1 p = P d = - ˙ i = I p = P
7 6 eqcomd p = P d = - ˙ i = I P = p
8 4 5 7 f1eq123d p = P d = - ˙ i = I f : 1 ..^ n 1-1 P f : 1 ..^ n 1-1 p
9 simp2 p = P d = - ˙ i = I d = - ˙
10 9 eqcomd p = P d = - ˙ i = I - ˙ = d
11 10 oveqd p = P d = - ˙ i = I f 1 - ˙ x = f 1 d x
12 10 oveqd p = P d = - ˙ i = I f j - ˙ x = f j d x
13 11 12 eqeq12d p = P d = - ˙ i = I f 1 - ˙ x = f j - ˙ x f 1 d x = f j d x
14 10 oveqd p = P d = - ˙ i = I f 1 - ˙ y = f 1 d y
15 10 oveqd p = P d = - ˙ i = I f j - ˙ y = f j d y
16 14 15 eqeq12d p = P d = - ˙ i = I f 1 - ˙ y = f j - ˙ y f 1 d y = f j d y
17 10 oveqd p = P d = - ˙ i = I f 1 - ˙ z = f 1 d z
18 10 oveqd p = P d = - ˙ i = I f j - ˙ z = f j d z
19 17 18 eqeq12d p = P d = - ˙ i = I f 1 - ˙ z = f j - ˙ z f 1 d z = f j d z
20 13 16 19 3anbi123d p = P d = - ˙ i = I f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z
21 20 ralbidv p = P d = - ˙ i = I j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z
22 simp3 p = P d = - ˙ i = I i = I
23 22 eqcomd p = P d = - ˙ i = I I = i
24 23 oveqd p = P d = - ˙ i = I x I y = x i y
25 24 eleq2d p = P d = - ˙ i = I z x I y z x i y
26 23 oveqd p = P d = - ˙ i = I z I y = z i y
27 26 eleq2d p = P d = - ˙ i = I x z I y x z i y
28 23 oveqd p = P d = - ˙ i = I x I z = x i z
29 28 eleq2d p = P d = - ˙ i = I y x I z y x i z
30 25 27 29 3orbi123d p = P d = - ˙ i = I z x I y x z I y y x I z z x i y x z i y y x i z
31 30 notbid p = P d = - ˙ i = I ¬ z x I y x z I y y x I z ¬ z x i y x z i y y x i z
32 21 31 anbi12d p = P d = - ˙ i = I j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
33 7 32 rexeqbidv p = P d = - ˙ i = I z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
34 7 33 rexeqbidv p = P d = - ˙ i = I y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
35 7 34 rexeqbidv p = P d = - ˙ i = I x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z x p y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
36 8 35 anbi12d p = P d = - ˙ i = I f : 1 ..^ n 1-1 P x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z f : 1 ..^ n 1-1 p x p y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
37 36 exbidv p = P d = - ˙ i = I f f : 1 ..^ n 1-1 P x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z f f : 1 ..^ n 1-1 p x p y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
38 1 2 3 37 sbcie3s g = G [˙Base g / p]˙ [˙ dist g / d]˙ [˙ Itv g / i]˙ f f : 1 ..^ n 1-1 p x p y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z f f : 1 ..^ n 1-1 P x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
39 eqidd n = N f = f
40 oveq2 n = N 1 ..^ n = 1 ..^ N
41 eqidd n = N P = P
42 39 40 41 f1eq123d n = N f : 1 ..^ n 1-1 P f : 1 ..^ N 1-1 P
43 oveq2 n = N 2 ..^ n = 2 ..^ N
44 43 raleqdv n = N j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z
45 44 anbi1d n = N j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
46 45 rexbidv n = N z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
47 46 2rexbidv n = N x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z x P y P z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
48 42 47 anbi12d n = N f : 1 ..^ n 1-1 P x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z f : 1 ..^ N 1-1 P x P y P z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
49 48 exbidv n = N f f : 1 ..^ n 1-1 P x P y P z P j 2 ..^ n f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z f f : 1 ..^ N 1-1 P x P y P z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z
50 df-trkgld Dim 𝒢 = g n | [˙Base g / p]˙ [˙ dist g / d]˙ [˙ Itv g / i]˙ f f : 1 ..^ n 1-1 p x p y p z p j 2 ..^ n f 1 d x = f j d x f 1 d y = f j d y f 1 d z = f j d z ¬ z x i y x z i y y x i z
51 38 49 50 brabg G V N 2 G Dim 𝒢 N f f : 1 ..^ N 1-1 P x P y P z P j 2 ..^ N f 1 - ˙ x = f j - ˙ x f 1 - ˙ y = f j - ˙ y f 1 - ˙ z = f j - ˙ z ¬ z x I y x z I y y x I z