afsval

Description: Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019)

	Ref	Expression
Hypotheses	brafs.p	$⊢ P = {Base}_{G}$
	brafs.d	$⊢ \underset{˙}{-} = dist (G)$
	brafs.i	$⊢ I = Itv (G)$
	brafs.g	$⊢ φ \to G \in 𝒢_{Tarski}$
Assertion	afsval	$⊢ φ \to AFS (G) = \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\}$

Proof

Step	Hyp	Ref	Expression
1		brafs.p	$⊢ P = {Base}_{G}$
2		brafs.d	$⊢ \underset{˙}{-} = dist (G)$
3		brafs.i	$⊢ I = Itv (G)$
4		brafs.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		df-afs	$⊢ AFS = (g \in 𝒢_{Tarski} ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\})$
6	5	a1i	$⊢ φ \to AFS = (g \in 𝒢_{Tarski} ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\})$
7		simp1	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to p = P$
8	7	eqcomd	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to P = p$
9	8	adantr	$⊢ ((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \to P = p$
10	9	adantr	$⊢ (((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \to P = p$
11	10	adantr	$⊢ ((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \to P = p$
12	11	adantr	$⊢ (((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \to P = p$
13	12	adantr	$⊢ ((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \to P = p$
14	13	adantr	$⊢ (((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \to P = p$
15	8	ad7antr	$⊢ ((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \to P = p$
16		simp3	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to i = I$
17	16	ad8antr	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to i = I$
18	17	eqcomd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to I = i$
19	18	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to a I c = a i c$
20	19	eleq2d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (b \in (a I c) \leftrightarrow b \in (a i c))$
21	18	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to x I z = x i z$
22	21	eleq2d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (y \in (x I z) \leftrightarrow y \in (x i z))$
23	20 22	anbi12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to ((b \in (a I c) \land y \in (x I z)) \leftrightarrow (b \in (a i c) \land y \in (x i z)))$
24		simp2	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to h = \underset{˙}{-}$
25	24	eqcomd	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to \underset{˙}{-} = h$
26	25	ad8antr	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to \underset{˙}{-} = h$
27	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to a \underset{˙}{-} b = a h b$
28	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to x \underset{˙}{-} y = x h y$
29	27 28	eqeq12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (a \underset{˙}{-} b = x \underset{˙}{-} y \leftrightarrow a h b = x h y)$
30	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to b \underset{˙}{-} c = b h c$
31	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to y \underset{˙}{-} z = y h z$
32	30 31	eqeq12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (b \underset{˙}{-} c = y \underset{˙}{-} z \leftrightarrow b h c = y h z)$
33	29 32	anbi12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to ((a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \leftrightarrow (a h b = x h y \land b h c = y h z))$
34	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to a \underset{˙}{-} d = a h d$
35	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to x \underset{˙}{-} w = x h w$
36	34 35	eqeq12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (a \underset{˙}{-} d = x \underset{˙}{-} w \leftrightarrow a h d = x h w)$
37	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to b \underset{˙}{-} d = b h d$
38	26	oveqd	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to y \underset{˙}{-} w = y h w$
39	37 38	eqeq12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (b \underset{˙}{-} d = y \underset{˙}{-} w \leftrightarrow b h d = y h w)$
40	36 39	anbi12d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to ((a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w) \leftrightarrow (a h d = x h w \land b h d = y h w))$
41	23 33 40	3anbi123d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to (((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)) \leftrightarrow ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
42	41	3anbi3d	$⊢ (((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \to ((e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
43	15 42	rexeqbidva	$⊢ ((((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \to (\exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
44	14 43	rexeqbidva	$⊢ (((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \to (\exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
45	13 44	rexeqbidva	$⊢ ((((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \land x \in P) \to (\exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
46	12 45	rexeqbidva	$⊢ (((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \land d \in P) \to (\exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
47	11 46	rexeqbidva	$⊢ ((((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \land c \in P) \to (\exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
48	10 47	rexeqbidva	$⊢ (((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \land b \in P) \to (\exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
49	9 48	rexeqbidva	$⊢ ((p = P \land h = \underset{˙}{-} \land i = I) \land a \in P) \to (\exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
50	8 49	rexeqbidva	$⊢ (p = P \land h = \underset{˙}{-} \land i = I) \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \leftrightarrow \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))))$
51	1 2 3 50	sbcie3s	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))) \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))))$
52	51	adantl	$⊢ (φ \land g = G) \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))) \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))))$
53	52	opabbidv	$⊢ (φ \land g = G) \to \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\} = \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\}$
54		df-xp	$⊢ ((P \times P) \times (P \times P)) \times ((P \times P) \times (P \times P)) = \{⟨e, f⟩ \| (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))\}$
55	1	fvexi	$⊢ P \in V$
56	55 55	xpex	$⊢ P \times P \in V$
57	56 56	xpex	$⊢ (P \times P) \times (P \times P) \in V$
58	57 57	xpex	$⊢ ((P \times P) \times (P \times P)) \times ((P \times P) \times (P \times P)) \in V$
59	54 58	eqeltrri	$⊢ \{⟨e, f⟩ \| (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))\} \in V$
60		3simpa	$⊢ (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
61	60	reximi	$⊢ \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
62	61	reximi	$⊢ \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
63	62	reximi	$⊢ \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
64	63	reximi	$⊢ \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
65	64	reximi	$⊢ \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
66	65	reximi	$⊢ \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
67	66	reximi	$⊢ \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
68	67	reximi	$⊢ \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)$
69		simpr	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to e = ⟨⟨a, b⟩, ⟨c, d⟩⟩$
70		opelxpi	$⊢ (a \in P \land b \in P) \to ⟨a, b⟩ \in (P \times P)$
71	70	ad7antr	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to ⟨a, b⟩ \in (P \times P)$
72		simp-7r	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to c \in P$
73		simp-6r	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to d \in P$
74		opelxpi	$⊢ (c \in P \land d \in P) \to ⟨c, d⟩ \in (P \times P)$
75	72 73 74	syl2anc	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to ⟨c, d⟩ \in (P \times P)$
76		opelxpi	$⊢ (⟨a, b⟩ \in (P \times P) \land ⟨c, d⟩ \in (P \times P)) \to ⟨⟨a, b⟩, ⟨c, d⟩⟩ \in ((P \times P) \times (P \times P))$
77	71 75 76	syl2anc	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to ⟨⟨a, b⟩, ⟨c, d⟩⟩ \in ((P \times P) \times (P \times P))$
78	69 77	eqeltrd	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land e = ⟨⟨a, b⟩, ⟨c, d⟩⟩) \to e \in ((P \times P) \times (P \times P))$
79		simpr	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to f = ⟨⟨x, y⟩, ⟨z, w⟩⟩$
80		simp-5r	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to x \in P$
81		simp-4r	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to y \in P$
82		opelxpi	$⊢ (x \in P \land y \in P) \to ⟨x, y⟩ \in (P \times P)$
83	80 81 82	syl2anc	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to ⟨x, y⟩ \in (P \times P)$
84		simpllr	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to z \in P$
85		simplr	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to w \in P$
86		opelxpi	$⊢ (z \in P \land w \in P) \to ⟨z, w⟩ \in (P \times P)$
87	84 85 86	syl2anc	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to ⟨z, w⟩ \in (P \times P)$
88		opelxpi	$⊢ (⟨x, y⟩ \in (P \times P) \land ⟨z, w⟩ \in (P \times P)) \to ⟨⟨x, y⟩, ⟨z, w⟩⟩ \in ((P \times P) \times (P \times P))$
89	83 87 88	syl2anc	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to ⟨⟨x, y⟩, ⟨z, w⟩⟩ \in ((P \times P) \times (P \times P))$
90	79 89	eqeltrd	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to f \in ((P \times P) \times (P \times P))$
91	78 90	anim12dan	$⊢ ((((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \land w \in P) \land (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩)) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))$
92	91	rexlimdva2	$⊢ ((((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \land z \in P) \to (\exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
93	92	rexlimdva	$⊢ (((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \land y \in P) \to (\exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
94	93	rexlimdva	$⊢ ((((a \in P \land b \in P) \land c \in P) \land d \in P) \land x \in P) \to (\exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
95	94	rexlimdva	$⊢ (((a \in P \land b \in P) \land c \in P) \land d \in P) \to (\exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
96	95	rexlimdva	$⊢ ((a \in P \land b \in P) \land c \in P) \to (\exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
97	96	rexlimdva	$⊢ (a \in P \land b \in P) \to (\exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P))))$
98	97	rexlimivv	$⊢ \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))$
99	68 98	syl	$⊢ \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w))) \to (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))$
100	99	ssopab2i	$⊢ \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\} \subseteq \{⟨e, f⟩ \| (e \in ((P \times P) \times (P \times P)) \land f \in ((P \times P) \times (P \times P)))\}$
101	59 100	ssexi	$⊢ \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\} \in V$
102	101	a1i	$⊢ φ \to \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\} \in V$
103	6 53 4 102	fvmptd	$⊢ φ \to AFS (G) = \{⟨e, f⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists x \in P \exists y \in P \exists z \in P \exists w \in P (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a I c) \land y \in (x I z)) \land (a \underset{˙}{-} b = x \underset{˙}{-} y \land b \underset{˙}{-} c = y \underset{˙}{-} z) \land (a \underset{˙}{-} d = x \underset{˙}{-} w \land b \underset{˙}{-} d = y \underset{˙}{-} w)))\}$

Metamath Proof Explorer

Theorem afsval

Proof