hypcgrlem2

Description: Lemma for hypcgr , case where triangles share one vertex B . (Contributed by Thierry Arnoux, 16-Dec-2019)

	Ref	Expression
Hypotheses	hypcgr.p	$⊢ P = {Base}_{G}$
	hypcgr.m	$⊢ \underset{˙}{-} = dist (G)$
	hypcgr.i	$⊢ I = Itv (G)$
	hypcgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hypcgr.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	hypcgr.a	$⊢ φ \to A \in P$
	hypcgr.b	$⊢ φ \to B \in P$
	hypcgr.c	$⊢ φ \to C \in P$
	hypcgr.d	$⊢ φ \to D \in P$
	hypcgr.e	$⊢ φ \to E \in P$
	hypcgr.f	$⊢ φ \to F \in P$
	hypcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	hypcgr.2	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
	hypcgr.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
	hypcgr.4	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$
	hypcgrlem2.b	$⊢ φ \to B = E$
	hypcgrlem2.s	$⊢ S = {lInv}_{𝒢} (G) ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B)$
Assertion	hypcgrlem2	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$

Proof

Step	Hyp	Ref	Expression
1		hypcgr.p	$⊢ P = {Base}_{G}$
2		hypcgr.m	$⊢ \underset{˙}{-} = dist (G)$
3		hypcgr.i	$⊢ I = Itv (G)$
4		hypcgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hypcgr.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		hypcgr.a	$⊢ φ \to A \in P$
7		hypcgr.b	$⊢ φ \to B \in P$
8		hypcgr.c	$⊢ φ \to C \in P$
9		hypcgr.d	$⊢ φ \to D \in P$
10		hypcgr.e	$⊢ φ \to E \in P$
11		hypcgr.f	$⊢ φ \to F \in P$
12		hypcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
13		hypcgr.2	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
14		hypcgr.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
15		hypcgr.4	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$
16		hypcgrlem2.b	$⊢ φ \to B = E$
17		hypcgrlem2.s	$⊢ S = {lInv}_{𝒢} (G) ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B)$
18	4	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to G \in 𝒢_{Tarski}$
19	5	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to G {Dim}_{𝒢} \geq 2$
20	6	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to A \in P$
21	7	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to B \in P$
22	8	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to C \in P$
23		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
24		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
25		eqid	$⊢ {pInv}_{𝒢} (G) (B) = {pInv}_{𝒢} (G) (B)$
26	9	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to D \in P$
27	1 2 3 23 24 18 21 25 26	mircl	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) \in P$
28	10	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to E \in P$
29	12	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
30		eqidd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) = {pInv}_{𝒢} (G) (B) (D)$
31	16	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to B = E$
32	1 2 3 23 24 18 21 25 28	mirinv	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ({pInv}_{𝒢} (G) (B) (E) = E \leftrightarrow B = E)$
33	31 32	mpbird	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (E) = E$
34	33	eqcomd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to E = {pInv}_{𝒢} (G) (B) (E)$
35	11	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to F \in P$
36	1 2 3 18 19 22 35	midcom	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to C {mid}_{𝒢} (G) F = F {mid}_{𝒢} (G) C$
37		simpr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to C {mid}_{𝒢} (G) F = B$
38	36 37	eqtr3d	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to F {mid}_{𝒢} (G) C = B$
39	1 2 3 18 19 35 22 24 21	ismidb	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to (C = {pInv}_{𝒢} (G) (B) (F) \leftrightarrow F {mid}_{𝒢} (G) C = B)$
40	38 39	mpbird	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to C = {pInv}_{𝒢} (G) (B) (F)$
41	30 34 40	s3eqd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ⟨“ {pInv}_{𝒢} (G) (B) (D) E C ”⟩ = ⟨“ {pInv}_{𝒢} (G) (B) (D) {pInv}_{𝒢} (G) (B) (E) {pInv}_{𝒢} (G) (B) (F) ”⟩$
42	13	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
43	1 2 3 23 24 18 26 28 35 42 25 21	mirrag	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ⟨“ {pInv}_{𝒢} (G) (B) (D) {pInv}_{𝒢} (G) (B) (E) {pInv}_{𝒢} (G) (B) (F) ”⟩ \in ∟_{𝒢} (G)$
44	41 43	eqeltrd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to ⟨“ {pInv}_{𝒢} (G) (B) (D) E C ”⟩ \in ∟_{𝒢} (G)$
45	14	adantr	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
46	1 2 3 23 24 18 21 25 26 28	miriso	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (E) = D \underset{˙}{-} E$
47	33	oveq2d	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (E) = {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} E$
48	45 46 47	3eqtr2d	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to A \underset{˙}{-} B = {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} E$
49	31	oveq1d	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to B \underset{˙}{-} C = E \underset{˙}{-} C$
50		eqid	$⊢ {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) {pInv}_{𝒢} (G) (B) (D)) {Line}_{𝒢} (G) B) = {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) {pInv}_{𝒢} (G) (B) (D)) {Line}_{𝒢} (G) B)$
51		eqidd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to C = C$
52	1 2 3 18 19 20 21 22 27 28 22 29 44 48 49 31 50 51	hypcgrlem1	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to A \underset{˙}{-} C = {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} C$
53	40	oveq2d	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} C = {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (F)$
54	1 2 3 23 24 18 21 25 26 35	miriso	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to {pInv}_{𝒢} (G) (B) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (F) = D \underset{˙}{-} F$
55	52 53 54	3eqtrd	$⊢ (φ \land C {mid}_{𝒢} (G) F = B) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
56	4	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to G \in 𝒢_{Tarski}$
57	5	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to G {Dim}_{𝒢} \geq 2$
58	6	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to A \in P$
59	7	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to B \in P$
60	8	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to C \in P$
61	9	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to D \in P$
62	10	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to E \in P$
63	11	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to F \in P$
64	12	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
65	13	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
66	14	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
67	15	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
68	16	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to B = E$
69		eqid	$⊢ {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) = {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
70		simpr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to C = F$
71	1 2 3 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70	hypcgrlem1	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = F) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
72	4	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to G \in 𝒢_{Tarski}$
73	5	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to G {Dim}_{𝒢} \geq 2$
74	6	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to A \in P$
75	7	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \in P$
76	8	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C \in P$
77	11	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to F \in P$
78	1 2 3 72 73 76 77	midcl	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in P$
79		simplr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \neq B$
80	1 3 23 72 78 75 79	tgelrnln	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to (C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B \in ran {Line}_{𝒢} (G)$
81	9	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to D \in P$
82	1 2 3 72 73 17 23 80 81	lmicl	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (D) \in P$
83	10	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to E \in P$
84	1 2 3 72 73 17 23 80 83	lmicl	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (E) \in P$
85	1 2 3 72 73 17 23 80 77	lmicl	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (F) \in P$
86	12	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
87	1 2 3 72 73 17 23 80	lmimot	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S \in (G Ismt G)$
88	13	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
89	1 2 3 23 24 72 81 83 77 87 88	motrag	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to ⟨“ S (D) S (E) S (F) ”⟩ \in ∟_{𝒢} (G)$
90	14	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
91	1 2 3 72 73 17 23 80 81 83	lmiiso	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (D) \underset{˙}{-} S (E) = D \underset{˙}{-} E$
92	90 91	eqtr4d	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to A \underset{˙}{-} B = S (D) \underset{˙}{-} S (E)$
93	15	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
94	1 2 3 72 73 17 23 80 83 77	lmiiso	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (E) \underset{˙}{-} S (F) = E \underset{˙}{-} F$
95	93 94	eqtr4d	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \underset{˙}{-} C = S (E) \underset{˙}{-} S (F)$
96	1 3 23 72 78 75 79	tglinerflx2	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \in ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B)$
97	1 2 3 72 73 17 23 80 75 96	lmicinv	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (B) = B$
98	16	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B = E$
99	98	fveq2d	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (B) = S (E)$
100	97 99	eqtr3d	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B = S (E)$
101		eqid	$⊢ {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) S (D)) {Line}_{𝒢} (G) B) = {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) S (D)) {Line}_{𝒢} (G) B)$
102	1 2 3 72 73 76 77	midcom	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F = F {mid}_{𝒢} (G) C$
103	1 3 23 72 78 75 79	tglinerflx1	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B)$
104	102 103	eqeltrrd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to F {mid}_{𝒢} (G) C \in ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B)$
105		simpr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C \neq F$
106	105	necomd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to F \neq C$
107	1 3 23 72 77 76 106	tgelrnln	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to F {Line}_{𝒢} (G) C \in ran {Line}_{𝒢} (G)$
108	1 2 3 72 73 76 77	midbtwn	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in (C I F)$
109	1 2 3 72 76 78 77 108	tgbtwncom	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in (F I C)$
110	1 3 23 72 77 76 78 106 109	btwnlng1	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in (F {Line}_{𝒢} (G) C)$
111	103 110	elind	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F \in (((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B) \cap (F {Line}_{𝒢} (G) C))$
112	1 3 23 72 77 76 106	tglinerflx2	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C \in (F {Line}_{𝒢} (G) C)$
113	79	necomd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \neq C {mid}_{𝒢} (G) F$
114	4	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to G \in 𝒢_{Tarski}$
115	8	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C \in P$
116	11	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to F \in P$
117	5	ad2antrr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to G {Dim}_{𝒢} \geq 2$
118		simpr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C = C {mid}_{𝒢} (G) F$
119	118	eqcomd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C {mid}_{𝒢} (G) F = C$
120	1 2 3 114 117 115 116 119	midcgr	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C \underset{˙}{-} C = C \underset{˙}{-} F$
121	120	eqcomd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C \underset{˙}{-} F = C \underset{˙}{-} C$
122	1 2 3 114 115 116 115 121	axtgcgrid	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C = C {mid}_{𝒢} (G) F) \to C = F$
123	122	ex	$⊢ (φ \land C {mid}_{𝒢} (G) F \neq B) \to (C = C {mid}_{𝒢} (G) F \to C = F)$
124	123	necon3d	$⊢ (φ \land C {mid}_{𝒢} (G) F \neq B) \to (C \neq F \to C \neq C {mid}_{𝒢} (G) F)$
125	124	imp	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C \neq C {mid}_{𝒢} (G) F$
126	98	eqcomd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to E = B$
127		eqidd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C {mid}_{𝒢} (G) F = C {mid}_{𝒢} (G) F$
128	1 2 3 72 73 76 77 24 78	ismidb	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to (F = {pInv}_{𝒢} (G) (C {mid}_{𝒢} (G) F) (C) \leftrightarrow C {mid}_{𝒢} (G) F = C {mid}_{𝒢} (G) F)$
129	127 128	mpbird	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to F = {pInv}_{𝒢} (G) (C {mid}_{𝒢} (G) F) (C)$
130	126 129	oveq12d	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to E \underset{˙}{-} F = B \underset{˙}{-} {pInv}_{𝒢} (G) (C {mid}_{𝒢} (G) F) (C)$
131	93 130	eqtrd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to B \underset{˙}{-} C = B \underset{˙}{-} {pInv}_{𝒢} (G) (C {mid}_{𝒢} (G) F) (C)$
132	1 2 3 23 24 72 75 78 76	israg	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to (⟨“ B (C {mid}_{𝒢} (G) F) C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow B \underset{˙}{-} C = B \underset{˙}{-} {pInv}_{𝒢} (G) (C {mid}_{𝒢} (G) F) (C))$
133	131 132	mpbird	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to ⟨“ B (C {mid}_{𝒢} (G) F) C ”⟩ \in ∟_{𝒢} (G)$
134	1 2 3 23 72 80 107 111 96 112 113 125 133	ragperp	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (F {Line}_{𝒢} (G) C)$
135	134	orcd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to (((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (F {Line}_{𝒢} (G) C) \lor F = C)$
136	1 2 3 72 73 17 23 80 77 76	islmib	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to (C = S (F) \leftrightarrow (F {mid}_{𝒢} (G) C \in ((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B) \land (((C {mid}_{𝒢} (G) F) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (F {Line}_{𝒢} (G) C) \lor F = C)))$
137	104 135 136	mpbir2and	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to C = S (F)$
138	1 2 3 72 73 74 75 76 82 84 85 86 89 92 95 100 101 137	hypcgrlem1	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to A \underset{˙}{-} C = S (D) \underset{˙}{-} S (F)$
139	1 2 3 72 73 17 23 80 81 77	lmiiso	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to S (D) \underset{˙}{-} S (F) = D \underset{˙}{-} F$
140	138 139	eqtrd	$⊢ ((φ \land C {mid}_{𝒢} (G) F \neq B) \land C \neq F) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
141	71 140	pm2.61dane	$⊢ (φ \land C {mid}_{𝒢} (G) F \neq B) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
142	55 141	pm2.61dane	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$

Metamath Proof Explorer

Theorem hypcgrlem2

Proof