lmieu

Description: Uniqueness of the line mirror point. Theorem 10.2 of Schwabhauser p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	$⊢ P = {Base}_{G}$
	ismid.d	$⊢ \underset{˙}{-} = dist (G)$
	ismid.i	$⊢ I = Itv (G)$
	ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	lmieu.l	$⊢ L = {Line}_{𝒢} (G)$
	lmieu.1	$⊢ φ \to D \in ran L$
	lmieu.a	$⊢ φ \to A \in P$
Assertion	lmieu	$⊢ φ \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$

Proof

Step	Hyp	Ref	Expression
1		ismid.p	$⊢ P = {Base}_{G}$
2		ismid.d	$⊢ \underset{˙}{-} = dist (G)$
3		ismid.i	$⊢ I = Itv (G)$
4		ismid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		ismid.1	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		lmieu.l	$⊢ L = {Line}_{𝒢} (G)$
7		lmieu.1	$⊢ φ \to D \in ran L$
8		lmieu.a	$⊢ φ \to A \in P$
9	8	adantr	$⊢ (φ \land A \in D) \to A \in P$
10		simpr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to \neg A = b$
11		eqidd	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A {mid}_{𝒢} (G) b = A {mid}_{𝒢} (G) b$
12	4	ad4antr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to G \in 𝒢_{Tarski}$
13	5	ad4antr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to G {Dim}_{𝒢} \geq 2$
14	9	ad3antrrr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A \in P$
15		simpllr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to b \in P$
16		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
17	1 2 3 12 13 14 15	midcl	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A {mid}_{𝒢} (G) b \in P$
18	1 2 3 12 13 14 15 16 17	ismidb	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to (b = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) b) (A) \leftrightarrow A {mid}_{𝒢} (G) b = A {mid}_{𝒢} (G) b)$
19	11 18	mpbird	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to b = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) b) (A)$
20	19	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to b = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) b) (A)$
21	12	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to G \in 𝒢_{Tarski}$
22	7	ad4antr	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to D \in ran L$
23	22	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to D \in ran L$
24	14	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A \in P$
25	15	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to b \in P$
26	10	neqned	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A \neq b$
27	26	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A \neq b$
28	1 3 6 21 24 25 27	tgelrnln	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A L b \in ran L$
29		simpr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to D \neq A L b$
30		simp-4r	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A \in D$
31	30	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A \in D$
32	1 3 6 21 24 25 27	tglinerflx1	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A \in (A L b)$
33	31 32	elind	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A \in (D \cap (A L b))$
34		simpllr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A {mid}_{𝒢} (G) b \in D$
35	1 2 3 12 13 14 15	midbtwn	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A {mid}_{𝒢} (G) b \in (A I b)$
36	1 3 6 12 14 15 17 26 35	btwnlng1	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to A {mid}_{𝒢} (G) b \in (A L b)$
37	36	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A {mid}_{𝒢} (G) b \in (A L b)$
38	34 37	elind	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A {mid}_{𝒢} (G) b \in (D \cap (A L b))$
39	1 3 6 21 23 28 29 33 38	tglineineq	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A = A {mid}_{𝒢} (G) b$
40	39	fveq2d	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to {pInv}_{𝒢} (G) (A) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) b)$
41	40	fveq1d	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to {pInv}_{𝒢} (G) (A) (A) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) b) (A)$
42		eqid	$⊢ {pInv}_{𝒢} (G) (A) = {pInv}_{𝒢} (G) (A)$
43	1 2 3 6 16 21 24 42	mircinv	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to {pInv}_{𝒢} (G) (A) (A) = A$
44	20 41 43	3eqtr2rd	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D \neq A L b) \to A = b$
45	10 44	mtand	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to \neg D \neq A L b$
46	4	ad5antr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to G \in 𝒢_{Tarski}$
47	7	ad5antr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to D \in ran L$
48		nne	$⊢ \neg D \neq A L b \leftrightarrow D = A L b$
49	45 48	sylib	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to D = A L b$
50	49	adantr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to D = A L b$
51	50 47	eqeltrrd	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to A L b \in ran L$
52		simpr	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to D ⟂_{𝒢} (G) (A L b)$
53	1 2 3 6 46 47 51 52	perpneq	$⊢ (((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \land D ⟂_{𝒢} (G) (A L b)) \to D \neq A L b$
54	45 53	mtand	$⊢ ((((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \land \neg A = b) \to \neg D ⟂_{𝒢} (G) (A L b)$
55	54	ex	$⊢ (((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \to (\neg A = b \to \neg D ⟂_{𝒢} (G) (A L b))$
56	55	con4d	$⊢ (((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \to (D ⟂_{𝒢} (G) (A L b) \to A = b)$
57		idd	$⊢ (((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \to (A = b \to A = b)$
58	56 57	jaod	$⊢ (((φ \land A \in D) \land b \in P) \land A {mid}_{𝒢} (G) b \in D) \to ((D ⟂_{𝒢} (G) (A L b) \lor A = b) \to A = b)$
59	58	impr	$⊢ (((φ \land A \in D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A = b$
60	59	eqcomd	$⊢ (((φ \land A \in D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to b = A$
61		simpr	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to b = A$
62	61	oveq2d	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A {mid}_{𝒢} (G) b = A {mid}_{𝒢} (G) A$
63	1 2 3 4 5 8 8	midid	$⊢ φ \to A {mid}_{𝒢} (G) A = A$
64	63	ad3antrrr	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A {mid}_{𝒢} (G) A = A$
65	62 64	eqtrd	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A {mid}_{𝒢} (G) b = A$
66		simpllr	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A \in D$
67	65 66	eqeltrd	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A {mid}_{𝒢} (G) b \in D$
68	61	eqcomd	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to A = b$
69	68	olcd	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to (D ⟂_{𝒢} (G) (A L b) \lor A = b)$
70	67 69	jca	$⊢ (((φ \land A \in D) \land b \in P) \land b = A) \to (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
71	60 70	impbida	$⊢ ((φ \land A \in D) \land b \in P) \to ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = A)$
72	71	ralrimiva	$⊢ (φ \land A \in D) \to \forall b \in P ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = A)$
73		reu6i	$⊢ (A \in P \land \forall b \in P ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = A)) \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
74	9 72 73	syl2anc	$⊢ (φ \land A \in D) \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
75	4	adantr	$⊢ (φ \land \neg A \in D) \to G \in 𝒢_{Tarski}$
76	75	ad2antrr	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to G \in 𝒢_{Tarski}$
77	7	adantr	$⊢ (φ \land \neg A \in D) \to D \in ran L$
78	77	ad2antrr	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to D \in ran L$
79		simplr	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to x \in D$
80	1 6 3 76 78 79	tglnpt	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to x \in P$
81		eqid	$⊢ {pInv}_{𝒢} (G) (x) = {pInv}_{𝒢} (G) (x)$
82	8	adantr	$⊢ (φ \land \neg A \in D) \to A \in P$
83	82	ad2antrr	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to A \in P$
84	1 2 3 6 16 76 80 81 83	mircl	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to {pInv}_{𝒢} (G) (x) (A) \in P$
85		oveq2	$⊢ x = A {mid}_{𝒢} (G) b \to A L x = A L (A {mid}_{𝒢} (G) b)$
86	85	breq1d	$⊢ x = A {mid}_{𝒢} (G) b \to ((A L x) ⟂_{𝒢} (G) D \leftrightarrow (A L (A {mid}_{𝒢} (G) b)) ⟂_{𝒢} (G) D)$
87		simprl	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b \in D$
88		simpr	$⊢ (φ \land \neg A \in D) \to \neg A \in D$
89	1 2 3 6 75 77 82 88	foot	$⊢ (φ \land \neg A \in D) \to \exists! x \in D (A L x) ⟂_{𝒢} (G) D$
90		reurmo	$⊢ \exists! x \in D (A L x) ⟂_{𝒢} (G) D \to \exists^{*} x \in D (A L x) ⟂_{𝒢} (G) D$
91	89 90	syl	$⊢ (φ \land \neg A \in D) \to \exists^{*} x \in D (A L x) ⟂_{𝒢} (G) D$
92	91	ad4antr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to \exists^{*} x \in D (A L x) ⟂_{𝒢} (G) D$
93	79	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to x \in D$
94		simpllr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (A L x) ⟂_{𝒢} (G) D$
95	76	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to G \in 𝒢_{Tarski}$
96	83	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A \in P$
97		simplr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to b \in P$
98	5	ad5antr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to G {Dim}_{𝒢} \geq 2$
99	1 2 3 95 98 96 97	midcl	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b \in P$
100	1 2 3 95 98 96 97	midbtwn	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b \in (A I b)$
101	88	ad4antr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to \neg A \in D$
102		nelne2	$⊢ (A {mid}_{𝒢} (G) b \in D \land \neg A \in D) \to A {mid}_{𝒢} (G) b \neq A$
103	87 101 102	syl2anc	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b \neq A$
104	1 2 3 95 96 99 97 100 103	tgbtwnne	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A \neq b$
105	1 3 6 95 96 97 99 104 100	btwnlng1	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b \in (A L b)$
106	1 3 6 95 96 97 104 99 103 105	tglineelsb2	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A L b = A L (A {mid}_{𝒢} (G) b)$
107	78	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to D \in ran L$
108	1 3 6 95 96 97 104	tgelrnln	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A L b \in ran L$
109	104	neneqd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to \neg A = b$
110		simprr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (D ⟂_{𝒢} (G) (A L b) \lor A = b)$
111	110	orcomd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (A = b \lor D ⟂_{𝒢} (G) (A L b))$
112	111	ord	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (\neg A = b \to D ⟂_{𝒢} (G) (A L b))$
113	109 112	mpd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to D ⟂_{𝒢} (G) (A L b)$
114	1 2 3 6 95 107 108 113	perpcom	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (A L b) ⟂_{𝒢} (G) D$
115	106 114	eqbrtrrd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (A L (A {mid}_{𝒢} (G) b)) ⟂_{𝒢} (G) D$
116	86 87 92 93 94 115	rmoi2	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to x = A {mid}_{𝒢} (G) b$
117	116	eqcomd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to A {mid}_{𝒢} (G) b = x$
118	80	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to x \in P$
119	1 2 3 95 98 96 97 16 118	ismidb	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to (b = {pInv}_{𝒢} (G) (x) (A) \leftrightarrow A {mid}_{𝒢} (G) b = x)$
120	117 119	mpbird	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))) \to b = {pInv}_{𝒢} (G) (x) (A)$
121		simpr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to b = {pInv}_{𝒢} (G) (x) (A)$
122	76	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to G \in 𝒢_{Tarski}$
123	5	ad5antr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to G {Dim}_{𝒢} \geq 2$
124	83	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to A \in P$
125		simplr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to b \in P$
126	80	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to x \in P$
127	1 2 3 122 123 124 125 16 126	ismidb	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to (b = {pInv}_{𝒢} (G) (x) (A) \leftrightarrow A {mid}_{𝒢} (G) b = x)$
128	121 127	mpbid	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to A {mid}_{𝒢} (G) b = x$
129	79	ad2antrr	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to x \in D$
130	128 129	eqeltrd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to A {mid}_{𝒢} (G) b \in D$
131	122	adantr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to G \in 𝒢_{Tarski}$
132		simp-4r	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to (A L x) ⟂_{𝒢} (G) D$
133	6 131 132	perpln1	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to A L x \in ran L$
134	78	ad3antrrr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to D \in ran L$
135	1 2 3 6 131 133 134 132	perpcom	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to D ⟂_{𝒢} (G) (A L x)$
136	124	adantr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to A \in P$
137	126	adantr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to x \in P$
138	1 3 6 131 136 137 133	tglnne	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to A \neq x$
139		simpllr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to b \in P$
140		simpr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to A \neq b$
141	140	necomd	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to b \neq A$
142	1 2 3 6 16 131 137 81 136	mirbtwn	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to x \in ({pInv}_{𝒢} (G) (x) (A) I A)$
143		simplr	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to b = {pInv}_{𝒢} (G) (x) (A)$
144	143	oveq1d	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to b I A = {pInv}_{𝒢} (G) (x) (A) I A$
145	142 144	eleqtrrd	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to x \in (b I A)$
146	1 3 6 131 139 136 137 141 145	btwnlng1	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to x \in (b L A)$
147	1 3 6 131 136 137 139 138 146 141	lnrot1	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to b \in (A L x)$
148	1 3 6 131 136 137 138 139 141 147	tglineelsb2	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to A L x = A L b$
149	135 148	breqtrd	$⊢ ((((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \land A \neq b) \to D ⟂_{𝒢} (G) (A L b)$
150	149	ex	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to (A \neq b \to D ⟂_{𝒢} (G) (A L b))$
151	150	necon1bd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to (\neg D ⟂_{𝒢} (G) (A L b) \to A = b)$
152	151	orrd	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to (D ⟂_{𝒢} (G) (A L b) \lor A = b)$
153	130 152	jca	$⊢ (((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \land b = {pInv}_{𝒢} (G) (x) (A)) \to (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
154	120 153	impbida	$⊢ ((((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \land b \in P) \to ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = {pInv}_{𝒢} (G) (x) (A))$
155	154	ralrimiva	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to \forall b \in P ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = {pInv}_{𝒢} (G) (x) (A))$
156		reu6i	$⊢ ({pInv}_{𝒢} (G) (x) (A) \in P \land \forall b \in P ((A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b)) \leftrightarrow b = {pInv}_{𝒢} (G) (x) (A))) \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
157	84 155 156	syl2anc	$⊢ (((φ \land \neg A \in D) \land x \in D) \land (A L x) ⟂_{𝒢} (G) D) \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
158	1 2 3 6 75 77 82 88	footex	$⊢ (φ \land \neg A \in D) \to \exists x \in D (A L x) ⟂_{𝒢} (G) D$
159	157 158	r19.29a	$⊢ (φ \land \neg A \in D) \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$
160	74 159	pm2.61dan	$⊢ φ \to \exists! b \in P (A {mid}_{𝒢} (G) b \in D \land (D ⟂_{𝒢} (G) (A L b) \lor A = b))$

Metamath Proof Explorer

Theorem lmieu

Proof