mirval

Description: Value of the point inversion function S . Definition 7.5 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-2019)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirval.a	$⊢ φ \to A \in P$
Assertion	mirval	$⊢ φ \to S (A) = (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y))))$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirval.a	$⊢ φ \to A \in P$
8		df-mir	$⊢ {pInv}_{𝒢} = (g \in V ⟼ (x \in {Base}_{g} ⟼ (y \in {Base}_{g} ⟼ (ι z \in {Base}_{g} \| (x dist (g) z = x dist (g) y \land x \in (z Itv (g) y))))))$
9		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
10	9 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
11		fveq2	$⊢ g = G \to dist (g) = dist (G)$
12	11 2	eqtr4di	$⊢ g = G \to dist (g) = \underset{˙}{-}$
13	12	oveqd	$⊢ g = G \to x dist (g) z = x \underset{˙}{-} z$
14	12	oveqd	$⊢ g = G \to x dist (g) y = x \underset{˙}{-} y$
15	13 14	eqeq12d	$⊢ g = G \to (x dist (g) z = x dist (g) y \leftrightarrow x \underset{˙}{-} z = x \underset{˙}{-} y)$
16		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
17	16 3	eqtr4di	$⊢ g = G \to Itv (g) = I$
18	17	oveqd	$⊢ g = G \to z Itv (g) y = z I y$
19	18	eleq2d	$⊢ g = G \to (x \in (z Itv (g) y) \leftrightarrow x \in (z I y))$
20	15 19	anbi12d	$⊢ g = G \to ((x dist (g) z = x dist (g) y \land x \in (z Itv (g) y)) \leftrightarrow (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))$
21	10 20	riotaeqbidv	$⊢ g = G \to (ι z \in {Base}_{g} \| (x dist (g) z = x dist (g) y \land x \in (z Itv (g) y))) = (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))$
22	10 21	mpteq12dv	$⊢ g = G \to (y \in {Base}_{g} ⟼ (ι z \in {Base}_{g} \| (x dist (g) z = x dist (g) y \land x \in (z Itv (g) y)))) = (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y))))$
23	10 22	mpteq12dv	$⊢ g = G \to (x \in {Base}_{g} ⟼ (y \in {Base}_{g} ⟼ (ι z \in {Base}_{g} \| (x dist (g) z = x dist (g) y \land x \in (z Itv (g) y))))) = (x \in P ⟼ (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))))$
24	6	elexd	$⊢ φ \to G \in V$
25	1	fvexi	$⊢ P \in V$
26	25	mptex	$⊢ (x \in P ⟼ (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y))))) \in V$
27	26	a1i	$⊢ φ \to (x \in P ⟼ (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y))))) \in V$
28	8 23 24 27	fvmptd3	$⊢ φ \to {pInv}_{𝒢} (G) = (x \in P ⟼ (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))))$
29	5 28	eqtrid	$⊢ φ \to S = (x \in P ⟼ (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))))$
30		simpll	$⊢ ((x = A \land y \in P) \land z \in P) \to x = A$
31	30	oveq1d	$⊢ ((x = A \land y \in P) \land z \in P) \to x \underset{˙}{-} z = A \underset{˙}{-} z$
32	30	oveq1d	$⊢ ((x = A \land y \in P) \land z \in P) \to x \underset{˙}{-} y = A \underset{˙}{-} y$
33	31 32	eqeq12d	$⊢ ((x = A \land y \in P) \land z \in P) \to (x \underset{˙}{-} z = x \underset{˙}{-} y \leftrightarrow A \underset{˙}{-} z = A \underset{˙}{-} y)$
34	30	eleq1d	$⊢ ((x = A \land y \in P) \land z \in P) \to (x \in (z I y) \leftrightarrow A \in (z I y))$
35	33 34	anbi12d	$⊢ ((x = A \land y \in P) \land z \in P) \to ((x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)) \leftrightarrow (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y)))$
36	35	riotabidva	$⊢ (x = A \land y \in P) \to (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y))) = (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y)))$
37	36	mpteq2dva	$⊢ x = A \to (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))) = (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y))))$
38	37	adantl	$⊢ (φ \land x = A) \to (y \in P ⟼ (ι z \in P \| (x \underset{˙}{-} z = x \underset{˙}{-} y \land x \in (z I y)))) = (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y))))$
39	25	mptex	$⊢ (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y)))) \in V$
40	39	a1i	$⊢ φ \to (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y)))) \in V$
41	29 38 7 40	fvmptd	$⊢ φ \to S (A) = (y \in P ⟼ (ι z \in P \| (A \underset{˙}{-} z = A \underset{˙}{-} y \land A \in (z I y))))$

Metamath Proof Explorer

Theorem mirval

Proof