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	$⊢ \underset{˙}{-} = dist (G)$
	istrkg.i	$⊢ I = Itv (G)$
Assertion	istrkgld	$⊢ (G \in V \land N \in ℤ_{\geq 2}) \to (G {Dim}_{𝒢} \geq N \leftrightarrow \exists f (f : (1 ..^N) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^N) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$

Proof

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

Metamath Proof Explorer

Theorem istrkgld

Proof