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=BaseG
israg.d -˙=distG
israg.i I=ItvG
israg.l L=Line𝒢G
israg.s S=pInv𝒢G
israg.g φG𝒢Tarski
israg.a φAP
israg.b φBP
israg.c φCP
ragflat.1 φ⟨“ABC”⟩𝒢G
ragflat.2 φ⟨“ACB”⟩𝒢G
Assertion ragflat φB=C

Proof

Step Hyp Ref Expression
1 israg.p P=BaseG
2 israg.d -˙=distG
3 israg.i I=ItvG
4 israg.l L=Line𝒢G
5 israg.s S=pInv𝒢G
6 israg.g φG𝒢Tarski
7 israg.a φAP
8 israg.b φBP
9 israg.c φCP
10 ragflat.1 φ⟨“ABC”⟩𝒢G
11 ragflat.2 φ⟨“ACB”⟩𝒢G
12 simpr φB=CB=C
13 6 adantr φBCG𝒢Tarski
14 7 adantr φBCAP
15 8 adantr φBCBP
16 9 adantr φBCCP
17 eqid SC=SC
18 1 2 3 4 5 13 16 17 14 mircl φBCSCAP
19 10 adantr φBC⟨“ABC”⟩𝒢G
20 1 2 3 4 5 13 16 17 14 mircgr φBCC-˙SCA=C-˙A
21 1 2 3 13 16 18 16 14 20 tgcgrcomlr φBCSCA-˙C=A-˙C
22 1 2 3 4 5 13 14 15 16 israg φBC⟨“ABC”⟩𝒢GA-˙C=A-˙SBC
23 19 22 mpbid φBCA-˙C=A-˙SBC
24 eqid SB=SB
25 1 2 3 4 5 13 15 24 16 mircl φBCSBCP
26 11 adantr φBC⟨“ACB”⟩𝒢G
27 1 2 3 4 5 13 14 16 15 26 ragcom φBC⟨“BCA”⟩𝒢G
28 simpr φBCBC
29 1 2 3 4 5 13 15 24 16 mirbtwn φBCBSBCIC
30 1 2 3 13 25 15 16 29 tgbtwncom φBCBCISBC
31 1 4 3 13 16 25 15 30 btwncolg1 φBCBCLSBCC=SBC
32 1 2 3 4 5 13 15 16 14 25 27 28 31 ragcol φBC⟨“SBCCA”⟩𝒢G
33 1 2 3 4 5 13 25 16 14 israg φBC⟨“SBCCA”⟩𝒢GSBC-˙A=SBC-˙SCA
34 32 33 mpbid φBCSBC-˙A=SBC-˙SCA
35 1 2 3 13 25 14 25 18 34 tgcgrcomlr φBCA-˙SBC=SCA-˙SBC
36 21 23 35 3eqtrd φBCSCA-˙C=SCA-˙SBC
37 1 2 3 4 5 13 18 15 16 israg φBC⟨“SCABC”⟩𝒢GSCA-˙C=SCA-˙SBC
38 36 37 mpbird φBC⟨“SCABC”⟩𝒢G
39 1 2 3 4 5 13 16 17 14 mirbtwn φBCCSCAIA
40 1 2 3 13 18 16 14 39 tgbtwncom φBCCAISCA
41 1 2 3 4 5 13 14 15 16 18 19 38 40 ragflat2 φBCB=C
42 12 41 pm2.61dane φB=C