Metamath Proof Explorer


Theorem ragcgr

Description: Right angle and colinearity. Theorem 8.10 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 4-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
ragcgr.c ˙=𝒢G
ragcgr.d φDP
ragcgr.e φEP
ragcgr.f φFP
ragcgr.1 φ⟨“ABC”⟩𝒢G
ragcgr.2 φ⟨“ABC”⟩˙⟨“DEF”⟩
Assertion ragcgr φ⟨“DEF”⟩𝒢G

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 ragcgr.c ˙=𝒢G
11 ragcgr.d φDP
12 ragcgr.e φEP
13 ragcgr.f φFP
14 ragcgr.1 φ⟨“ABC”⟩𝒢G
15 ragcgr.2 φ⟨“ABC”⟩˙⟨“DEF”⟩
16 eqidd φB=CD=D
17 6 adantr φB=CG𝒢Tarski
18 8 adantr φB=CBP
19 9 adantr φB=CCP
20 12 adantr φB=CEP
21 13 adantr φB=CFP
22 7 adantr φB=CAP
23 11 adantr φB=CDP
24 15 adantr φB=C⟨“ABC”⟩˙⟨“DEF”⟩
25 1 2 3 10 17 22 18 19 23 20 21 24 cgr3simp2 φB=CB-˙C=E-˙F
26 simpr φB=CB=C
27 1 2 3 17 18 19 20 21 25 26 tgcgreq φB=CE=F
28 eqidd φB=CF=F
29 16 27 28 s3eqd φB=C⟨“DEF”⟩=⟨“DFF”⟩
30 1 2 3 4 5 17 23 21 20 ragtrivb φB=C⟨“DFF”⟩𝒢G
31 29 30 eqeltrd φB=C⟨“DEF”⟩𝒢G
32 14 adantr φBC⟨“ABC”⟩𝒢G
33 6 adantr φBCG𝒢Tarski
34 7 adantr φBCAP
35 8 adantr φBCBP
36 9 adantr φBCCP
37 1 2 3 4 5 33 34 35 36 israg φBC⟨“ABC”⟩𝒢GA-˙C=A-˙SBC
38 32 37 mpbid φBCA-˙C=A-˙SBC
39 13 adantr φBCFP
40 11 adantr φBCDP
41 12 adantr φBCEP
42 15 adantr φBC⟨“ABC”⟩˙⟨“DEF”⟩
43 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp3 φBCC-˙A=F-˙D
44 1 2 3 33 36 34 39 40 43 tgcgrcomlr φBCA-˙C=D-˙F
45 eqid SB=SB
46 1 2 3 4 5 33 35 45 36 mircl φBCSBCP
47 eqid SE=SE
48 1 2 3 4 5 33 41 47 39 mircl φBCSEFP
49 simpr φBCBC
50 49 necomd φBCCB
51 1 2 3 4 5 33 35 45 36 mirbtwn φBCBSBCIC
52 1 2 3 33 46 35 36 51 tgbtwncom φBCBCISBC
53 1 2 3 4 5 33 41 47 39 mirbtwn φBCESEFIF
54 1 2 3 33 48 41 39 53 tgbtwncom φBCEFISEF
55 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp2 φBCB-˙C=E-˙F
56 1 2 3 33 35 36 41 39 55 tgcgrcomlr φBCC-˙B=F-˙E
57 1 2 3 4 5 33 35 45 36 mircgr φBCB-˙SBC=B-˙C
58 1 2 3 4 5 33 41 47 39 mircgr φBCE-˙SEF=E-˙F
59 55 57 58 3eqtr4d φBCB-˙SBC=E-˙SEF
60 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp1 φBCA-˙B=D-˙E
61 1 2 3 33 34 35 40 41 60 tgcgrcomlr φBCB-˙A=E-˙D
62 1 2 3 33 36 35 46 39 41 48 34 40 50 52 54 56 59 43 61 axtg5seg φBCSBC-˙A=SEF-˙D
63 1 2 3 33 46 34 48 40 62 tgcgrcomlr φBCA-˙SBC=D-˙SEF
64 38 44 63 3eqtr3d φBCD-˙F=D-˙SEF
65 1 2 3 4 5 33 40 41 39 israg φBC⟨“DEF”⟩𝒢GD-˙F=D-˙SEF
66 64 65 mpbird φBC⟨“DEF”⟩𝒢G
67 31 66 pm2.61dane φ⟨“DEF”⟩𝒢G