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 𝑃 = ( Base ‘ 𝐺 )
israg.d = ( dist ‘ 𝐺 )
israg.i 𝐼 = ( Itv ‘ 𝐺 )
israg.l 𝐿 = ( LineG ‘ 𝐺 )
israg.s 𝑆 = ( pInvG ‘ 𝐺 )
israg.g ( 𝜑𝐺 ∈ TarskiG )
israg.a ( 𝜑𝐴𝑃 )
israg.b ( 𝜑𝐵𝑃 )
israg.c ( 𝜑𝐶𝑃 )
ragflat2.d ( 𝜑𝐷𝑃 )
ragflat2.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragflat2.2 ( 𝜑 → ⟨“ 𝐷 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
ragflat2.3 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion ragflat2 ( 𝜑𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 israg.p 𝑃 = ( Base ‘ 𝐺 )
2 israg.d = ( dist ‘ 𝐺 )
3 israg.i 𝐼 = ( Itv ‘ 𝐺 )
4 israg.l 𝐿 = ( LineG ‘ 𝐺 )
5 israg.s 𝑆 = ( pInvG ‘ 𝐺 )
6 israg.g ( 𝜑𝐺 ∈ TarskiG )
7 israg.a ( 𝜑𝐴𝑃 )
8 israg.b ( 𝜑𝐵𝑃 )
9 israg.c ( 𝜑𝐶𝑃 )
10 ragflat2.d ( 𝜑𝐷𝑃 )
11 ragflat2.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
12 ragflat2.2 ( 𝜑 → ⟨“ 𝐷 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
13 ragflat2.3 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
14 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
15 eqid ( 𝑆𝐵 ) = ( 𝑆𝐵 )
16 1 2 3 4 5 6 8 15 9 mircl ( 𝜑 → ( ( 𝑆𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
17 1 2 3 4 5 6 7 8 9 israg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 𝐶 ) = ( 𝐴 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) ) )
18 11 17 mpbid ( 𝜑 → ( 𝐴 𝐶 ) = ( 𝐴 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) )
19 1 2 3 4 5 6 10 8 9 israg ( 𝜑 → ( ⟨“ 𝐷 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐷 𝐶 ) = ( 𝐷 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) ) )
20 12 19 mpbid ( 𝜑 → ( 𝐷 𝐶 ) = ( 𝐷 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) )
21 1 4 3 6 7 10 9 14 16 7 2 13 18 20 tgidinside ( 𝜑𝐶 = ( ( 𝑆𝐵 ) ‘ 𝐶 ) )
22 21 eqcomd ( 𝜑 → ( ( 𝑆𝐵 ) ‘ 𝐶 ) = 𝐶 )
23 1 2 3 4 5 6 8 15 9 mirinv ( 𝜑 → ( ( ( 𝑆𝐵 ) ‘ 𝐶 ) = 𝐶𝐵 = 𝐶 ) )
24 22 23 mpbid ( 𝜑𝐵 = 𝐶 )