colperpexlem1

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	colperpexlem.s	$⊢ S = {pInv}_{𝒢} (G)$
	colperpexlem.m	$⊢ M = S (A)$
	colperpexlem.n	$⊢ N = S (B)$
	colperpexlem.k	$⊢ K = S (Q)$
	colperpexlem.a	$⊢ φ \to A \in P$
	colperpexlem.b	$⊢ φ \to B \in P$
	colperpexlem.c	$⊢ φ \to C \in P$
	colperpexlem.q	$⊢ φ \to Q \in P$
	colperpexlem.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	colperpexlem.2	$⊢ φ \to K (M (C)) = N (C)$
Assertion	colperpexlem1	$⊢ φ \to ⟨“ B A Q ”⟩ \in ∟_{𝒢} (G)$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		colperpexlem.s	$⊢ S = {pInv}_{𝒢} (G)$
7		colperpexlem.m	$⊢ M = S (A)$
8		colperpexlem.n	$⊢ N = S (B)$
9		colperpexlem.k	$⊢ K = S (Q)$
10		colperpexlem.a	$⊢ φ \to A \in P$
11		colperpexlem.b	$⊢ φ \to B \in P$
12		colperpexlem.c	$⊢ φ \to C \in P$
13		colperpexlem.q	$⊢ φ \to Q \in P$
14		colperpexlem.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
15		colperpexlem.2	$⊢ φ \to K (M (C)) = N (C)$
16	1 2 3 4 6 5 10 7 13	mircl	$⊢ φ \to M (Q) \in P$
17	1 2 3 4 6 5 10 7 12	mircl	$⊢ φ \to M (C) \in P$
18		eqid	$⊢ S (B) = S (B)$
19	1 2 3 4 6 5 11 18 12	mircl	$⊢ φ \to S (B) (C) \in P$
20	1 2 3 4 6 5 10 7 19	mircl	$⊢ φ \to M (S (B) (C)) \in P$
21	1 2 3 4 6 5 11 8 12	mircl	$⊢ φ \to N (C) \in P$
22	15 21	eqeltrd	$⊢ φ \to K (M (C)) \in P$
23	1 2 3 4 6 5 13 9 17	mirbtwn	$⊢ φ \to Q \in (K (M (C)) I M (C))$
24	1 2 3 5 22 13 17 23	tgbtwncom	$⊢ φ \to Q \in (M (C) I K (M (C)))$
25	8	fveq1i	$⊢ N (C) = S (B) (C)$
26	15 25	eqtrdi	$⊢ φ \to K (M (C)) = S (B) (C)$
27	26	oveq2d	$⊢ φ \to M (C) I K (M (C)) = M (C) I S (B) (C)$
28	24 27	eleqtrd	$⊢ φ \to Q \in (M (C) I S (B) (C))$
29	1 2 3 5 17 13 19 28	tgbtwncom	$⊢ φ \to Q \in (S (B) (C) I M (C))$
30	1 2 3 4 6 5 10 7 19 13 17 29	mirbtwni	$⊢ φ \to M (Q) \in (M (S (B) (C)) I M (M (C)))$
31	1 2 3 4 6 5 10 7 12	mirmir	$⊢ φ \to M (M (C)) = C$
32	31	oveq2d	$⊢ φ \to M (S (B) (C)) I M (M (C)) = M (S (B) (C)) I C$
33	30 32	eleqtrd	$⊢ φ \to M (Q) \in (M (S (B) (C)) I C)$
34	1 2 3 5 17 19	axtgcgrrflx	$⊢ φ \to M (C) \underset{˙}{-} S (B) (C) = S (B) (C) \underset{˙}{-} M (C)$
35	1 2 3 4 6 5 10 7 19 17	miriso	$⊢ φ \to M (S (B) (C)) \underset{˙}{-} M (M (C)) = S (B) (C) \underset{˙}{-} M (C)$
36	31	oveq2d	$⊢ φ \to M (S (B) (C)) \underset{˙}{-} M (M (C)) = M (S (B) (C)) \underset{˙}{-} C$
37	34 35 36	3eqtr2d	$⊢ φ \to M (C) \underset{˙}{-} S (B) (C) = M (S (B) (C)) \underset{˙}{-} C$
38	26	oveq2d	$⊢ φ \to Q \underset{˙}{-} K (M (C)) = Q \underset{˙}{-} S (B) (C)$
39	1 2 3 4 6 5 13 9 17	mircgr	$⊢ φ \to Q \underset{˙}{-} K (M (C)) = Q \underset{˙}{-} M (C)$
40	38 39	eqtr3d	$⊢ φ \to Q \underset{˙}{-} S (B) (C) = Q \underset{˙}{-} M (C)$
41	1 2 3 4 6 5 10 7 13 17	miriso	$⊢ φ \to M (Q) \underset{˙}{-} M (M (C)) = Q \underset{˙}{-} M (C)$
42	31	oveq2d	$⊢ φ \to M (Q) \underset{˙}{-} M (M (C)) = M (Q) \underset{˙}{-} C$
43	40 41 42	3eqtr2d	$⊢ φ \to Q \underset{˙}{-} S (B) (C) = M (Q) \underset{˙}{-} C$
44	1 2 3 4 6 5 10 7 11	mirmir	$⊢ φ \to M (M (B)) = B$
45		eqidd	$⊢ φ \to M (B) = M (B)$
46		eqidd	$⊢ φ \to M (C) = M (C)$
47	44 45 46	s3eqd	$⊢ φ \to ⟨“ M (M (B)) M (B) M (C) ”⟩ = ⟨“ B M (B) M (C) ”⟩$
48	1 2 3 4 6 5 10 7 11	mircl	$⊢ φ \to M (B) \in P$
49		simpr	$⊢ (φ \land A = B) \to A = B$
50	49	fveq2d	$⊢ (φ \land A = B) \to M (A) = M (B)$
51	5	adantr	$⊢ (φ \land A = B) \to G \in 𝒢_{Tarski}$
52	10	adantr	$⊢ (φ \land A = B) \to A \in P$
53	1 2 3 4 6 51 52 7	mircinv	$⊢ (φ \land A = B) \to M (A) = A$
54	50 53	eqtr3d	$⊢ (φ \land A = B) \to M (B) = A$
55		eqidd	$⊢ (φ \land A = B) \to B = B$
56		eqidd	$⊢ (φ \land A = B) \to C = C$
57	54 55 56	s3eqd	$⊢ (φ \land A = B) \to ⟨“ M (B) B C ”⟩ = ⟨“ A B C ”⟩$
58	14	adantr	$⊢ (φ \land A = B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
59	57 58	eqeltrd	$⊢ (φ \land A = B) \to ⟨“ M (B) B C ”⟩ \in ∟_{𝒢} (G)$
60	5	adantr	$⊢ (φ \land A \neq B) \to G \in 𝒢_{Tarski}$
61	10	adantr	$⊢ (φ \land A \neq B) \to A \in P$
62	11	adantr	$⊢ (φ \land A \neq B) \to B \in P$
63	12	adantr	$⊢ (φ \land A \neq B) \to C \in P$
64	1 2 3 4 6 60 61 7 62	mircl	$⊢ (φ \land A \neq B) \to M (B) \in P$
65	14	adantr	$⊢ (φ \land A \neq B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
66		simpr	$⊢ (φ \land A \neq B) \to A \neq B$
67	1 2 3 4 6 60 61 7 62	mirbtwn	$⊢ (φ \land A \neq B) \to A \in (M (B) I B)$
68	1 4 3 60 64 62 61 67	btwncolg1	$⊢ (φ \land A \neq B) \to (A \in (M (B) L B) \lor M (B) = B)$
69	1 4 3 60 64 62 61 68	colcom	$⊢ (φ \land A \neq B) \to (A \in (B L M (B)) \lor B = M (B))$
70	1 2 3 4 6 60 61 62 63 64 65 66 69	ragcol	$⊢ (φ \land A \neq B) \to ⟨“ M (B) B C ”⟩ \in ∟_{𝒢} (G)$
71	59 70	pm2.61dane	$⊢ φ \to ⟨“ M (B) B C ”⟩ \in ∟_{𝒢} (G)$
72	1 2 3 4 6 5 48 11 12 71 7 10	mirrag	$⊢ φ \to ⟨“ M (M (B)) M (B) M (C) ”⟩ \in ∟_{𝒢} (G)$
73	47 72	eqeltrrd	$⊢ φ \to ⟨“ B M (B) M (C) ”⟩ \in ∟_{𝒢} (G)$
74	1 2 3 4 6 5 11 48 17	israg	$⊢ φ \to (⟨“ B M (B) M (C) ”⟩ \in ∟_{𝒢} (G) \leftrightarrow B \underset{˙}{-} M (C) = B \underset{˙}{-} S (M (B)) (M (C)))$
75	73 74	mpbid	$⊢ φ \to B \underset{˙}{-} M (C) = B \underset{˙}{-} S (M (B)) (M (C))$
76	1 2 3 4 6 5 10 7 12 11	mirmir2	$⊢ φ \to M (S (B) (C)) = S (M (B)) (M (C))$
77	76	oveq2d	$⊢ φ \to B \underset{˙}{-} M (S (B) (C)) = B \underset{˙}{-} S (M (B)) (M (C))$
78	75 77	eqtr4d	$⊢ φ \to B \underset{˙}{-} M (C) = B \underset{˙}{-} M (S (B) (C))$
79	1 2 3 5 11 17 11 20 78	tgcgrcomlr	$⊢ φ \to M (C) \underset{˙}{-} B = M (S (B) (C)) \underset{˙}{-} B$
80	1 2 3 4 6 5 11 18 12	mircgr	$⊢ φ \to B \underset{˙}{-} S (B) (C) = B \underset{˙}{-} C$
81	1 2 3 5 11 19 11 12 80	tgcgrcomlr	$⊢ φ \to S (B) (C) \underset{˙}{-} B = C \underset{˙}{-} B$
82	1 2 3 5 17 13 19 11 20 16 12 11 28 33 37 43 79 81	tgifscgr	$⊢ φ \to Q \underset{˙}{-} B = M (Q) \underset{˙}{-} B$
83	1 2 3 5 13 11 16 11 82	tgcgrcomlr	$⊢ φ \to B \underset{˙}{-} Q = B \underset{˙}{-} M (Q)$
84	7	fveq1i	$⊢ M (Q) = S (A) (Q)$
85	84	oveq2i	$⊢ B \underset{˙}{-} M (Q) = B \underset{˙}{-} S (A) (Q)$
86	83 85	eqtrdi	$⊢ φ \to B \underset{˙}{-} Q = B \underset{˙}{-} S (A) (Q)$
87	1 2 3 4 6 5 11 10 13	israg	$⊢ φ \to (⟨“ B A Q ”⟩ \in ∟_{𝒢} (G) \leftrightarrow B \underset{˙}{-} Q = B \underset{˙}{-} S (A) (Q))$
88	86 87	mpbird	$⊢ φ \to ⟨“ B A Q ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem colperpexlem1

Proof