Metamath Proof Explorer


Theorem ragflat

Description: Deduce equality from two right angles. Theorem 8.7 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019)

Ref Expression
Hypotheses israg.p P = Base G
israg.d - ˙ = dist G
israg.i I = Itv G
israg.l L = Line 𝒢 G
israg.s S = pInv 𝒢 G
israg.g φ G 𝒢 Tarski
israg.a φ A P
israg.b φ B P
israg.c φ C P
ragflat.1 φ ⟨“ ABC ”⟩ 𝒢 G
ragflat.2 φ ⟨“ ACB ”⟩ 𝒢 G
Assertion ragflat φ B = C

Proof

Step Hyp Ref Expression
1 israg.p P = Base G
2 israg.d - ˙ = dist G
3 israg.i I = Itv G
4 israg.l L = Line 𝒢 G
5 israg.s S = pInv 𝒢 G
6 israg.g φ G 𝒢 Tarski
7 israg.a φ A P
8 israg.b φ B P
9 israg.c φ C P
10 ragflat.1 φ ⟨“ ABC ”⟩ 𝒢 G
11 ragflat.2 φ ⟨“ ACB ”⟩ 𝒢 G
12 simpr φ B = C B = C
13 6 adantr φ B C G 𝒢 Tarski
14 7 adantr φ B C A P
15 8 adantr φ B C B P
16 9 adantr φ B C C P
17 eqid S C = S C
18 1 2 3 4 5 13 16 17 14 mircl φ B C S C A P
19 10 adantr φ B C ⟨“ ABC ”⟩ 𝒢 G
20 1 2 3 4 5 13 16 17 14 mircgr φ B C C - ˙ S C A = C - ˙ A
21 1 2 3 13 16 18 16 14 20 tgcgrcomlr φ B C S C A - ˙ C = A - ˙ C
22 1 2 3 4 5 13 14 15 16 israg φ B C ⟨“ ABC ”⟩ 𝒢 G A - ˙ C = A - ˙ S B C
23 19 22 mpbid φ B C A - ˙ C = A - ˙ S B C
24 eqid S B = S B
25 1 2 3 4 5 13 15 24 16 mircl φ B C S B C P
26 11 adantr φ B C ⟨“ ACB ”⟩ 𝒢 G
27 1 2 3 4 5 13 14 16 15 26 ragcom φ B C ⟨“ BCA ”⟩ 𝒢 G
28 simpr φ B C B C
29 1 2 3 4 5 13 15 24 16 mirbtwn φ B C B S B C I C
30 1 2 3 13 25 15 16 29 tgbtwncom φ B C B C I S B C
31 1 4 3 13 16 25 15 30 btwncolg1 φ B C B C L S B C C = S B C
32 1 2 3 4 5 13 15 16 14 25 27 28 31 ragcol φ B C ⟨“ S B C CA ”⟩ 𝒢 G
33 1 2 3 4 5 13 25 16 14 israg φ B C ⟨“ S B C CA ”⟩ 𝒢 G S B C - ˙ A = S B C - ˙ S C A
34 32 33 mpbid φ B C S B C - ˙ A = S B C - ˙ S C A
35 1 2 3 13 25 14 25 18 34 tgcgrcomlr φ B C A - ˙ S B C = S C A - ˙ S B C
36 21 23 35 3eqtrd φ B C S C A - ˙ C = S C A - ˙ S B C
37 1 2 3 4 5 13 18 15 16 israg φ B C ⟨“ S C A BC ”⟩ 𝒢 G S C A - ˙ C = S C A - ˙ S B C
38 36 37 mpbird φ B C ⟨“ S C A BC ”⟩ 𝒢 G
39 1 2 3 4 5 13 16 17 14 mirbtwn φ B C C S C A I A
40 1 2 3 13 18 16 14 39 tgbtwncom φ B C C A I S C A
41 1 2 3 4 5 13 14 15 16 18 19 38 40 ragflat2 φ B C B = C
42 12 41 pm2.61dane φ B = C