Metamath Proof Explorer


Theorem ragflat2

Description: Deduce equality from two right angles. Theorem 8.6 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
ragflat2.d φDP
ragflat2.1 φ⟨“ABC”⟩𝒢G
ragflat2.2 φ⟨“DBC”⟩𝒢G
ragflat2.3 φCAID
Assertion ragflat2 φ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 ragflat2.d φDP
11 ragflat2.1 φ⟨“ABC”⟩𝒢G
12 ragflat2.2 φ⟨“DBC”⟩𝒢G
13 ragflat2.3 φCAID
14 eqid 𝒢G=𝒢G
15 eqid SB=SB
16 1 2 3 4 5 6 8 15 9 mircl φSBCP
17 1 2 3 4 5 6 7 8 9 israg φ⟨“ABC”⟩𝒢GA-˙C=A-˙SBC
18 11 17 mpbid φA-˙C=A-˙SBC
19 1 2 3 4 5 6 10 8 9 israg φ⟨“DBC”⟩𝒢GD-˙C=D-˙SBC
20 12 19 mpbid φD-˙C=D-˙SBC
21 1 4 3 6 7 10 9 14 16 7 2 13 18 20 tgidinside φC=SBC
22 21 eqcomd φSBC=C
23 1 2 3 4 5 6 8 15 9 mirinv φSBC=CB=C
24 22 23 mpbid φB=C