trgcopyeulem

	Ref	Expression
Hypotheses	trgcopy.p	$⊢ P = {Base}_{G}$
	trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
	trgcopy.i	$⊢ I = Itv (G)$
	trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
	trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
	trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	trgcopy.a	$⊢ φ \to A \in P$
	trgcopy.b	$⊢ φ \to B \in P$
	trgcopy.c	$⊢ φ \to C \in P$
	trgcopy.d	$⊢ φ \to D \in P$
	trgcopy.e	$⊢ φ \to E \in P$
	trgcopy.f	$⊢ φ \to F \in P$
	trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
	trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
	trgcopyeulem.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (D L E)) \land b \in (P ∖ (D L E))) \land \exists t \in (D L E) t \in (a I b))\}$
	trgcopyeulem.x	$⊢ φ \to X \in P$
	trgcopyeulem.y	$⊢ φ \to Y \in P$
	trgcopyeulem.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E X ”⟩$
	trgcopyeulem.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E Y ”⟩$
	trgcopyeulem.3	$⊢ φ \to X {hp}_{𝒢} (G) (D L E) F$
	trgcopyeulem.4	$⊢ φ \to Y {hp}_{𝒢} (G) (D L E) F$
Assertion	trgcopyeulem	$⊢ φ \to X = Y$

Proof

Step	Hyp	Ref	Expression
1		trgcopy.p	$⊢ P = {Base}_{G}$
2		trgcopy.m	$⊢ \underset{˙}{-} = dist (G)$
3		trgcopy.i	$⊢ I = Itv (G)$
4		trgcopy.l	$⊢ L = {Line}_{𝒢} (G)$
5		trgcopy.k	$⊢ K = {hl}_{𝒢} (G)$
6		trgcopy.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		trgcopy.a	$⊢ φ \to A \in P$
8		trgcopy.b	$⊢ φ \to B \in P$
9		trgcopy.c	$⊢ φ \to C \in P$
10		trgcopy.d	$⊢ φ \to D \in P$
11		trgcopy.e	$⊢ φ \to E \in P$
12		trgcopy.f	$⊢ φ \to F \in P$
13		trgcopy.1	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
14		trgcopy.2	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
15		trgcopy.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
16		trgcopyeulem.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (D L E)) \land b \in (P ∖ (D L E))) \land \exists t \in (D L E) t \in (a I b))\}$
17		trgcopyeulem.x	$⊢ φ \to X \in P$
18		trgcopyeulem.y	$⊢ φ \to Y \in P$
19		trgcopyeulem.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E X ”⟩$
20		trgcopyeulem.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ D E Y ”⟩$
21		trgcopyeulem.3	$⊢ φ \to X {hp}_{𝒢} (G) (D L E) F$
22		trgcopyeulem.4	$⊢ φ \to Y {hp}_{𝒢} (G) (D L E) F$
23	1 4 3 6 8 9 7 13	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
24		eqid	$⊢ {lInv}_{𝒢} (G) (D L E) = {lInv}_{𝒢} (G) (D L E)$
25	1 3 4 6 10 11 12 14	ncolne1	$⊢ φ \to D \neq E$
26	1 3 4 6 10 11 25	tgelrnln	$⊢ φ \to D L E \in ran L$
27		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
28	6	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to G \in 𝒢_{Tarski}$
29	26	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D L E \in ran L$
30		simplr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in (D L E)$
31	1 4 3 28 29 30	tglnpt	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in P$
32		eqid	$⊢ {pInv}_{𝒢} (G) (t) = {pInv}_{𝒢} (G) (t)$
33	1 2 3 6 23 24 4 26 18	lmicl	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (Y) \in P$
34	33	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to {lInv}_{𝒢} (G) (D L E) (Y) \in P$
35	17	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X \in P$
36	10	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D \in P$
37	11	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to E \in P$
38		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
39	25	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D \neq E$
40	39	necomd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to E \neq D$
41	1 3 4 28 37 36 31 40 30	lncom	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in (E L D)$
42	41	orcd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to (t \in (E L D) \lor E = D)$
43	1 4 3 28 37 36 31 42	colrot1	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to (E \in (D L t) \lor D = t)$
44	1 2 3 38 6 7 8 9 10 11 17 19	cgr3simp3	$⊢ φ \to C \underset{˙}{-} A = X \underset{˙}{-} D$
45	1 2 3 6 9 7 17 10 44	tgcgrcomlr	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} X$
46	1 2 3 38 6 7 8 9 10 11 18 20	cgr3simp3	$⊢ φ \to C \underset{˙}{-} A = Y \underset{˙}{-} D$
47	1 2 3 6 9 7 18 10 46	tgcgrcomlr	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} Y$
48	45 47	eqtr3d	$⊢ φ \to D \underset{˙}{-} X = D \underset{˙}{-} Y$
49	1 2 3 6 23 24 4 26 10 18	lmiiso	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (D) \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = D \underset{˙}{-} Y$
50	1 3 4 6 10 11 25	tglinerflx1	$⊢ φ \to D \in (D L E)$
51	1 2 3 6 23 24 4 26 10 50	lmicinv	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (D) = D$
52	51	oveq1d	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (D) \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = D \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
53	48 49 52	3eqtr2d	$⊢ φ \to D \underset{˙}{-} X = D \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
54	53	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D \underset{˙}{-} X = D \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
55	1 2 3 38 6 7 8 9 10 11 17 19	cgr3simp2	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} X$
56	1 2 3 38 6 7 8 9 10 11 18 20	cgr3simp2	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} Y$
57	55 56	eqtr3d	$⊢ φ \to E \underset{˙}{-} X = E \underset{˙}{-} Y$
58	1 2 3 6 23 24 4 26 11 18	lmiiso	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (E) \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = E \underset{˙}{-} Y$
59	1 3 4 6 10 11 25	tglinerflx2	$⊢ φ \to E \in (D L E)$
60	1 2 3 6 23 24 4 26 11 59	lmicinv	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (E) = E$
61	60	oveq1d	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (E) \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = E \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
62	57 58 61	3eqtr2d	$⊢ φ \to E \underset{˙}{-} X = E \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
63	62	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to E \underset{˙}{-} X = E \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
64	1 4 3 28 36 37 31 38 35 34 2 39 43 54 63	lncgr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \underset{˙}{-} X = t \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y)$
65		simpr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))$
66	1 2 3 4 27 28 31 32 34 35 64 65	ismir	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X = {pInv}_{𝒢} (G) (t) ({lInv}_{𝒢} (G) (D L E) (Y))$
67	66	eqcomd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to {pInv}_{𝒢} (G) (t) ({lInv}_{𝒢} (G) (D L E) (Y)) = X$
68	1 2 3 4 27 28 31 32 34 67	mircom	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to {pInv}_{𝒢} (G) (t) (X) = {lInv}_{𝒢} (G) (D L E) (Y)$
69	68	eqcomd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to {lInv}_{𝒢} (G) (D L E) (Y) = {pInv}_{𝒢} (G) (t) (X)$
70	23	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to G {Dim}_{𝒢} \geq 2$
71	1 2 3 28 70 35 34 27 31	ismidb	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to ({lInv}_{𝒢} (G) (D L E) (Y) = {pInv}_{𝒢} (G) (t) (X) \leftrightarrow X {mid}_{𝒢} (G) {lInv}_{𝒢} (G) (D L E) (Y) = t)$
72	69 71	mpbid	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X {mid}_{𝒢} (G) {lInv}_{𝒢} (G) (D L E) (Y) = t$
73	72 30	eqeltrd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X {mid}_{𝒢} (G) {lInv}_{𝒢} (G) (D L E) (Y) \in (D L E)$
74	1 3 4 6 26 17 16 12 21	hpgcom	$⊢ φ \to F {hp}_{𝒢} (G) (D L E) X$
75	1 3 4 6 26 18 16 12 22 17 74	hpgtr	$⊢ φ \to Y {hp}_{𝒢} (G) (D L E) X$
76	1 3 4 16 6 26 18 12 22	hpgne1	$⊢ φ \to \neg Y \in (D L E)$
77	1 2 3 4 6 23 26 16 24 18 76	lmiopp	$⊢ φ \to Y O {lInv}_{𝒢} (G) (D L E) (Y)$
78	1 3 4 16 6 26 18 17 33 77	lnopp2hpgb	$⊢ φ \to (X O {lInv}_{𝒢} (G) (D L E) (Y) \leftrightarrow Y {hp}_{𝒢} (G) (D L E) X)$
79	75 78	mpbird	$⊢ φ \to X O {lInv}_{𝒢} (G) (D L E) (Y)$
80	1 2 3 16 17 33	islnopp	$⊢ φ \to (X O {lInv}_{𝒢} (G) (D L E) (Y) \leftrightarrow ((\neg X \in (D L E) \land \neg {lInv}_{𝒢} (G) (D L E) (Y) \in (D L E)) \land \exists t \in (D L E) t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))))$
81	79 80	mpbid	$⊢ φ \to ((\neg X \in (D L E) \land \neg {lInv}_{𝒢} (G) (D L E) (Y) \in (D L E)) \land \exists t \in (D L E) t \in (X I {lInv}_{𝒢} (G) (D L E) (Y)))$
82	81	simprd	$⊢ φ \to \exists t \in (D L E) t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))$
83	73 82	r19.29a	$⊢ φ \to X {mid}_{𝒢} (G) {lInv}_{𝒢} (G) (D L E) (Y) \in (D L E)$
84	28	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to G \in 𝒢_{Tarski}$
85	29	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to D L E \in ran L$
86	1 2 3 16 4 26 6 17 33 79	oppne3	$⊢ φ \to X \neq {lInv}_{𝒢} (G) (D L E) (Y)$
87	1 3 4 6 17 33 86	tgelrnln	$⊢ φ \to X L {lInv}_{𝒢} (G) (D L E) (Y) \in ran L$
88	87	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X L {lInv}_{𝒢} (G) (D L E) (Y) \in ran L$
89	88	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to X L {lInv}_{𝒢} (G) (D L E) (Y) \in ran L$
90	86	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X \neq {lInv}_{𝒢} (G) (D L E) (Y)$
91	1 3 4 28 35 34 31 90 65	btwnlng1	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in (X L {lInv}_{𝒢} (G) (D L E) (Y))$
92	30 91	elind	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \in ((D L E) \cap (X L {lInv}_{𝒢} (G) (D L E) (Y)))$
93	92	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to t \in ((D L E) \cap (X L {lInv}_{𝒢} (G) (D L E) (Y)))$
94	59	ad3antrrr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to E \in (D L E)$
95	1 3 4 6 17 33 86	tglinerflx1	$⊢ φ \to X \in (X L {lInv}_{𝒢} (G) (D L E) (Y))$
96	95	ad3antrrr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to X \in (X L {lInv}_{𝒢} (G) (D L E) (Y))$
97		simpr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to E \neq t$
98	81	simplld	$⊢ φ \to \neg X \in (D L E)$
99	98	ad2antrr	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to \neg X \in (D L E)$
100		nelne2	$⊢ (t \in (D L E) \land \neg X \in (D L E)) \to t \neq X$
101	30 99 100	syl2anc	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to t \neq X$
102	101	necomd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to X \neq t$
103	102	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to X \neq t$
104	69	oveq2d	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to E \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = E \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
105	63 104	eqtrd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to E \underset{˙}{-} X = E \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
106	105	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to E \underset{˙}{-} X = E \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
107	37	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to E \in P$
108	31	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to t \in P$
109	35	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to X \in P$
110	1 2 3 4 27 84 107 108 109	israg	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to (⟨“ E t X ”⟩ \in ∟_{𝒢} (G) \leftrightarrow E \underset{˙}{-} X = E \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X))$
111	106 110	mpbird	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to ⟨“ E t X ”⟩ \in ∟_{𝒢} (G)$
112	1 2 3 4 84 85 89 93 94 96 97 103 111	ragperp	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land E \neq t) \to (D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y))$
113	28	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to G \in 𝒢_{Tarski}$
114	29	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to D L E \in ran L$
115	88	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to X L {lInv}_{𝒢} (G) (D L E) (Y) \in ran L$
116	92	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to t \in ((D L E) \cap (X L {lInv}_{𝒢} (G) (D L E) (Y)))$
117	50	ad3antrrr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to D \in (D L E)$
118	95	ad3antrrr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to X \in (X L {lInv}_{𝒢} (G) (D L E) (Y))$
119		simpr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to D \neq t$
120	102	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to X \neq t$
121	69	oveq2d	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D \underset{˙}{-} {lInv}_{𝒢} (G) (D L E) (Y) = D \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
122	54 121	eqtrd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to D \underset{˙}{-} X = D \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
123	122	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to D \underset{˙}{-} X = D \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X)$
124	36	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to D \in P$
125	31	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to t \in P$
126	35	adantr	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to X \in P$
127	1 2 3 4 27 113 124 125 126	israg	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to (⟨“ D t X ”⟩ \in ∟_{𝒢} (G) \leftrightarrow D \underset{˙}{-} X = D \underset{˙}{-} {pInv}_{𝒢} (G) (t) (X))$
128	123 127	mpbird	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to ⟨“ D t X ”⟩ \in ∟_{𝒢} (G)$
129	1 2 3 4 113 114 115 116 117 118 119 120 128	ragperp	$⊢ (((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \land D \neq t) \to (D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y))$
130		neneor	$⊢ E \neq D \to (E \neq t \lor D \neq t)$
131	40 130	syl	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to (E \neq t \lor D \neq t)$
132	112 129 131	mpjaodan	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to (D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y))$
133	132	orcd	$⊢ ((φ \land t \in (D L E)) \land t \in (X I {lInv}_{𝒢} (G) (D L E) (Y))) \to ((D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y)) \lor X = {lInv}_{𝒢} (G) (D L E) (Y))$
134	133 82	r19.29a	$⊢ φ \to ((D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y)) \lor X = {lInv}_{𝒢} (G) (D L E) (Y))$
135	1 2 3 6 23 24 4 26 17 33	islmib	$⊢ φ \to ({lInv}_{𝒢} (G) (D L E) (Y) = {lInv}_{𝒢} (G) (D L E) (X) \leftrightarrow (X {mid}_{𝒢} (G) {lInv}_{𝒢} (G) (D L E) (Y) \in (D L E) \land ((D L E) ⟂_{𝒢} (G) (X L {lInv}_{𝒢} (G) (D L E) (Y)) \lor X = {lInv}_{𝒢} (G) (D L E) (Y))))$
136	83 134 135	mpbir2and	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (Y) = {lInv}_{𝒢} (G) (D L E) (X)$
137	136	eqcomd	$⊢ φ \to {lInv}_{𝒢} (G) (D L E) (X) = {lInv}_{𝒢} (G) (D L E) (Y)$
138	1 2 3 6 23 24 4 26 17 18 137	lmieq	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem trgcopyeulem

Proof