hypcgrlem1

Description: Lemma for hypcgr , case where triangles share a cathetus. (Contributed by Thierry Arnoux, 15-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$
	hypcgrlem1.s	$⊢ S = {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
	hypcgrlem1.a	$⊢ φ \to C = F$
Assertion	hypcgrlem1	$⊢ φ \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		hypcgrlem1.s	$⊢ S = {lInv}_{𝒢} (G) ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
18		hypcgrlem1.a	$⊢ φ \to C = F$
19	4	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to G \in 𝒢_{Tarski}$
20	8	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to C \in P$
21	6	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to A \in P$
22	11	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to F \in P$
23	9	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to D \in P$
24		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
25		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
26	1 2 3 24 25 4 6 7 8 12	ragcom	$⊢ φ \to ⟨“ C B A ”⟩ \in ∟_{𝒢} (G)$
27	1 2 3 24 25 4 8 7 6	israg	$⊢ φ \to (⟨“ C B A ”⟩ \in ∟_{𝒢} (G) \leftrightarrow C \underset{˙}{-} A = C \underset{˙}{-} {pInv}_{𝒢} (G) (B) (A))$
28	26 27	mpbid	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} {pInv}_{𝒢} (G) (B) (A)$
29	28	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to C \underset{˙}{-} A = C \underset{˙}{-} {pInv}_{𝒢} (G) (B) (A)$
30	18	eqcomd	$⊢ φ \to F = C$
31	30	adantr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to F = C$
32	1 2 3 4 5 6 9 25 7	ismidb	$⊢ φ \to (D = {pInv}_{𝒢} (G) (B) (A) \leftrightarrow A {mid}_{𝒢} (G) D = B)$
33	32	biimpar	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to D = {pInv}_{𝒢} (G) (B) (A)$
34	31 33	oveq12d	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to F \underset{˙}{-} D = C \underset{˙}{-} {pInv}_{𝒢} (G) (B) (A)$
35	29 34	eqtr4d	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to C \underset{˙}{-} A = F \underset{˙}{-} D$
36	1 2 3 19 20 21 22 23 35	tgcgrcomlr	$⊢ (φ \land A {mid}_{𝒢} (G) D = B) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
37		simpr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = D) \to A = D$
38	18	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = D) \to C = F$
39	37 38	oveq12d	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = D) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
40	12	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
41	4	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to G \in 𝒢_{Tarski}$
42	6	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \in P$
43	7	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \in P$
44	8	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to C \in P$
45	1 2 3 24 25 41 42 43 44	israg	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C))$
46	40 45	mpbid	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} C = A \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C)$
47	5	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to G {Dim}_{𝒢} \geq 2$
48	9	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D \in P$
49	1 2 3 41 47 42 48	midcl	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in P$
50		simplr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \neq B$
51	1 3 24 41 49 43 50	tgelrnln	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B \in ran {Line}_{𝒢} (G)$
52		eqid	$⊢ {pInv}_{𝒢} (G) (B) = {pInv}_{𝒢} (G) (B)$
53		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
54	1 2 3 24 25 41 43 52 44	mircl	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to {pInv}_{𝒢} (G) (B) (C) \in P$
55		simpr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \neq D$
56	1 2 3 41 47 42 48	midbtwn	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in (A I D)$
57	1 24 3 41 42 49 48 56	btwncolg3	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (D \in (A {Line}_{𝒢} (G) (A {mid}_{𝒢} (G) D)) \lor A = A {mid}_{𝒢} (G) D)$
58		eqidd	$⊢ φ \to D = D$
59	58 16 18	s3eqd	$⊢ φ \to ⟨“ D B C ”⟩ = ⟨“ D E F ”⟩$
60	59	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ D B C ”⟩ = ⟨“ D E F ”⟩$
61	13	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
62	60 61	eqeltrd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ D B C ”⟩ \in ∟_{𝒢} (G)$
63	1 2 3 24 25 41 48 43 44	israg	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (⟨“ D B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow D \underset{˙}{-} C = D \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C))$
64	62 63	mpbid	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D \underset{˙}{-} C = D \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C)$
65	1 24 3 41 42 48 49 53 44 54 2 55 57 46 64	lncgr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (A {mid}_{𝒢} (G) D) \underset{˙}{-} C = (A {mid}_{𝒢} (G) D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C)$
66	1 2 3 24 25 41 49 43 44	israg	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (⟨“ (A {mid}_{𝒢} (G) D) B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow (A {mid}_{𝒢} (G) D) \underset{˙}{-} C = (A {mid}_{𝒢} (G) D) \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C))$
67	65 66	mpbird	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ (A {mid}_{𝒢} (G) D) B C ”⟩ \in ∟_{𝒢} (G)$
68	1 3 24 41 49 43 50	tglinerflx1	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
69	1 3 24 41 49 43 50	tglinerflx2	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \in ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
70	1 2 3 41 47 17 24 51 49 52 67 68 69 44 50	lmimid	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to S (C) = {pInv}_{𝒢} (G) (B) (C)$
71	70	oveq2d	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} S (C) = A \underset{˙}{-} {pInv}_{𝒢} (G) (B) (C)$
72	46 71	eqtr4d	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} C = A \underset{˙}{-} S (C)$
73	1 2 3 41 47 48 42	midcom	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D {mid}_{𝒢} (G) A = A {mid}_{𝒢} (G) D$
74	73 68	eqeltrd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D {mid}_{𝒢} (G) A \in ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B)$
75	55	necomd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D \neq A$
76	1 3 24 41 48 42 75	tgelrnln	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D {Line}_{𝒢} (G) A \in ran {Line}_{𝒢} (G)$
77	1 2 3 41 42 49 48 56	tgbtwncom	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in (D I A)$
78	1 3 24 41 48 42 49 75 77	btwnlng1	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in (D {Line}_{𝒢} (G) A)$
79	68 78	elind	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D \in (((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) \cap (D {Line}_{𝒢} (G) A))$
80	1 3 24 41 48 42 75	tglinerflx2	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \in (D {Line}_{𝒢} (G) A)$
81	50	necomd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \neq A {mid}_{𝒢} (G) D$
82	4	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to G \in 𝒢_{Tarski}$
83	6	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A \in P$
84	9	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to D \in P$
85	5	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to G {Dim}_{𝒢} \geq 2$
86		simpr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A = A {mid}_{𝒢} (G) D$
87	86	eqcomd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A {mid}_{𝒢} (G) D = A$
88	1 2 3 82 85 83 84 87	midcgr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A \underset{˙}{-} A = A \underset{˙}{-} D$
89	88	eqcomd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A \underset{˙}{-} D = A \underset{˙}{-} A$
90	1 2 3 82 83 84 83 89	axtgcgrid	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A = A {mid}_{𝒢} (G) D) \to A = D$
91	90	ex	$⊢ (φ \land A {mid}_{𝒢} (G) D \neq B) \to (A = A {mid}_{𝒢} (G) D \to A = D)$
92	91	necon3d	$⊢ (φ \land A {mid}_{𝒢} (G) D \neq B) \to (A \neq D \to A \neq A {mid}_{𝒢} (G) D)$
93	92	imp	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \neq A {mid}_{𝒢} (G) D$
94	1 2 3 4 6 7 9 10 14	tgcgrcomlr	$⊢ φ \to B \underset{˙}{-} A = E \underset{˙}{-} D$
95	16	oveq1d	$⊢ φ \to B \underset{˙}{-} D = E \underset{˙}{-} D$
96	94 95	eqtr4d	$⊢ φ \to B \underset{˙}{-} A = B \underset{˙}{-} D$
97	96	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \underset{˙}{-} A = B \underset{˙}{-} D$
98		eqidd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A {mid}_{𝒢} (G) D = A {mid}_{𝒢} (G) D$
99	1 2 3 41 47 42 48 25 49	ismidb	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (D = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) D) (A) \leftrightarrow A {mid}_{𝒢} (G) D = A {mid}_{𝒢} (G) D)$
100	98 99	mpbird	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) D) (A)$
101	100	oveq2d	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \underset{˙}{-} D = B \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) D) (A)$
102	97 101	eqtrd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to B \underset{˙}{-} A = B \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) D) (A)$
103	1 2 3 24 25 41 43 49 42	israg	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (⟨“ B (A {mid}_{𝒢} (G) D) A ”⟩ \in ∟_{𝒢} (G) \leftrightarrow B \underset{˙}{-} A = B \underset{˙}{-} {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) D) (A))$
104	102 103	mpbird	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ⟨“ B (A {mid}_{𝒢} (G) D) A ”⟩ \in ∟_{𝒢} (G)$
105	1 2 3 24 41 51 76 79 69 80 81 93 104	ragperp	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (D {Line}_{𝒢} (G) A)$
106	105	orcd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (D {Line}_{𝒢} (G) A) \lor D = A)$
107	1 2 3 41 47 17 24 51 48 42	islmib	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to (A = S (D) \leftrightarrow (D {mid}_{𝒢} (G) A \in ((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) \land (((A {mid}_{𝒢} (G) D) {Line}_{𝒢} (G) B) ⟂_{𝒢} (G) (D {Line}_{𝒢} (G) A) \lor D = A)))$
108	74 106 107	mpbir2and	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A = S (D)$
109	108	oveq1d	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} S (C) = S (D) \underset{˙}{-} S (C)$
110	1 2 3 41 47 17 24 51 48 44	lmiiso	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to S (D) \underset{˙}{-} S (C) = D \underset{˙}{-} C$
111	18	oveq2d	$⊢ φ \to D \underset{˙}{-} C = D \underset{˙}{-} F$
112	111	ad2antrr	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to D \underset{˙}{-} C = D \underset{˙}{-} F$
113	109 110 112	3eqtrd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} S (C) = D \underset{˙}{-} F$
114	72 113	eqtrd	$⊢ ((φ \land A {mid}_{𝒢} (G) D \neq B) \land A \neq D) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
115	39 114	pm2.61dane	$⊢ (φ \land A {mid}_{𝒢} (G) D \neq B) \to A \underset{˙}{-} C = D \underset{˙}{-} F$
116	36 115	pm2.61dane	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$

Metamath Proof Explorer

Theorem hypcgrlem1

Proof