Metamath Proof Explorer


Theorem trgcgrg

Description: The property for two triangles to be congruent to each other. (Contributed by Thierry Arnoux, 3-Apr-2019)

Ref Expression
Hypotheses trgcgrg.p P=BaseG
trgcgrg.m -˙=distG
trgcgrg.r ˙=𝒢G
trgcgrg.g φG𝒢Tarski
trgcgrg.a φAP
trgcgrg.b φBP
trgcgrg.c φCP
trgcgrg.d φDP
trgcgrg.e φEP
trgcgrg.f φFP
Assertion trgcgrg φ⟨“ABC”⟩˙⟨“DEF”⟩A-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D

Proof

Step Hyp Ref Expression
1 trgcgrg.p P=BaseG
2 trgcgrg.m -˙=distG
3 trgcgrg.r ˙=𝒢G
4 trgcgrg.g φG𝒢Tarski
5 trgcgrg.a φAP
6 trgcgrg.b φBP
7 trgcgrg.c φCP
8 trgcgrg.d φDP
9 trgcgrg.e φEP
10 trgcgrg.f φFP
11 5 6 7 s3cld φ⟨“ABC”⟩WordP
12 wrdf ⟨“ABC”⟩WordP⟨“ABC”⟩:0..^⟨“ABC”⟩P
13 11 12 syl φ⟨“ABC”⟩:0..^⟨“ABC”⟩P
14 s3len ⟨“ABC”⟩=3
15 14 oveq2i 0..^⟨“ABC”⟩=0..^3
16 fzo0to3tp 0..^3=012
17 15 16 eqtri 0..^⟨“ABC”⟩=012
18 17 feq2i ⟨“ABC”⟩:0..^⟨“ABC”⟩P⟨“ABC”⟩:012P
19 13 18 sylib φ⟨“ABC”⟩:012P
20 19 fdmd φdom⟨“ABC”⟩=012
21 20 raleqdv φjdom⟨“ABC”⟩⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩jj012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j
22 20 21 raleqbidv φidom⟨“ABC”⟩jdom⟨“ABC”⟩⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩ji012j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j
23 0re 0
24 1re 1
25 2re 2
26 tpssi 012012
27 23 24 25 26 mp3an 012
28 27 a1i φ012
29 8 9 10 s3cld φ⟨“DEF”⟩WordP
30 wrdf ⟨“DEF”⟩WordP⟨“DEF”⟩:0..^⟨“DEF”⟩P
31 29 30 syl φ⟨“DEF”⟩:0..^⟨“DEF”⟩P
32 s3len ⟨“DEF”⟩=3
33 32 oveq2i 0..^⟨“DEF”⟩=0..^3
34 33 16 eqtri 0..^⟨“DEF”⟩=012
35 34 feq2i ⟨“DEF”⟩:0..^⟨“DEF”⟩P⟨“DEF”⟩:012P
36 31 35 sylib φ⟨“DEF”⟩:012P
37 1 2 3 4 28 19 36 iscgrgd φ⟨“ABC”⟩˙⟨“DEF”⟩idom⟨“ABC”⟩jdom⟨“ABC”⟩⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j
38 fveq2 j=0⟨“ABC”⟩j=⟨“ABC”⟩0
39 s3fv0 AP⟨“ABC”⟩0=A
40 5 39 syl φ⟨“ABC”⟩0=A
41 38 40 sylan9eqr φj=0⟨“ABC”⟩j=A
42 41 oveq2d φj=0⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“ABC”⟩i-˙A
43 fveq2 j=0⟨“DEF”⟩j=⟨“DEF”⟩0
44 s3fv0 DP⟨“DEF”⟩0=D
45 8 44 syl φ⟨“DEF”⟩0=D
46 43 45 sylan9eqr φj=0⟨“DEF”⟩j=D
47 46 oveq2d φj=0⟨“DEF”⟩i-˙⟨“DEF”⟩j=⟨“DEF”⟩i-˙D
48 42 47 eqeq12d φj=0⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D
49 fveq2 j=1⟨“ABC”⟩j=⟨“ABC”⟩1
50 s3fv1 BP⟨“ABC”⟩1=B
51 6 50 syl φ⟨“ABC”⟩1=B
52 49 51 sylan9eqr φj=1⟨“ABC”⟩j=B
53 52 oveq2d φj=1⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“ABC”⟩i-˙B
54 fveq2 j=1⟨“DEF”⟩j=⟨“DEF”⟩1
55 s3fv1 EP⟨“DEF”⟩1=E
56 9 55 syl φ⟨“DEF”⟩1=E
57 54 56 sylan9eqr φj=1⟨“DEF”⟩j=E
58 57 oveq2d φj=1⟨“DEF”⟩i-˙⟨“DEF”⟩j=⟨“DEF”⟩i-˙E
59 53 58 eqeq12d φj=1⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E
60 fveq2 j=2⟨“ABC”⟩j=⟨“ABC”⟩2
61 s3fv2 CP⟨“ABC”⟩2=C
62 7 61 syl φ⟨“ABC”⟩2=C
63 60 62 sylan9eqr φj=2⟨“ABC”⟩j=C
64 63 oveq2d φj=2⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“ABC”⟩i-˙C
65 fveq2 j=2⟨“DEF”⟩j=⟨“DEF”⟩2
66 s3fv2 FP⟨“DEF”⟩2=F
67 10 66 syl φ⟨“DEF”⟩2=F
68 65 67 sylan9eqr φj=2⟨“DEF”⟩j=F
69 68 oveq2d φj=2⟨“DEF”⟩i-˙⟨“DEF”⟩j=⟨“DEF”⟩i-˙F
70 64 69 eqeq12d φj=2⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
71 0red φ0
72 1red φ1
73 25 a1i φ2
74 48 59 70 71 72 73 raltpd φj012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
75 74 adantr φi=0j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
76 fveq2 i=0⟨“ABC”⟩i=⟨“ABC”⟩0
77 76 adantl φi=0⟨“ABC”⟩i=⟨“ABC”⟩0
78 40 adantr φi=0⟨“ABC”⟩0=A
79 77 78 eqtr2d φi=0A=⟨“ABC”⟩i
80 79 oveq1d φi=0A-˙A=⟨“ABC”⟩i-˙A
81 fveq2 i=0⟨“DEF”⟩i=⟨“DEF”⟩0
82 81 adantl φi=0⟨“DEF”⟩i=⟨“DEF”⟩0
83 45 adantr φi=0⟨“DEF”⟩0=D
84 82 83 eqtr2d φi=0D=⟨“DEF”⟩i
85 84 oveq1d φi=0D-˙D=⟨“DEF”⟩i-˙D
86 80 85 eqeq12d φi=0A-˙A=D-˙D⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D
87 79 oveq1d φi=0A-˙B=⟨“ABC”⟩i-˙B
88 84 oveq1d φi=0D-˙E=⟨“DEF”⟩i-˙E
89 87 88 eqeq12d φi=0A-˙B=D-˙E⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E
90 79 oveq1d φi=0A-˙C=⟨“ABC”⟩i-˙C
91 84 oveq1d φi=0D-˙F=⟨“DEF”⟩i-˙F
92 90 91 eqeq12d φi=0A-˙C=D-˙F⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
93 86 89 92 3anbi123d φi=0A-˙A=D-˙DA-˙B=D-˙EA-˙C=D-˙F⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
94 75 93 bitr4d φi=0j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩jA-˙A=D-˙DA-˙B=D-˙EA-˙C=D-˙F
95 74 adantr φi=1j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
96 fveq2 i=1⟨“ABC”⟩i=⟨“ABC”⟩1
97 96 adantl φi=1⟨“ABC”⟩i=⟨“ABC”⟩1
98 51 adantr φi=1⟨“ABC”⟩1=B
99 97 98 eqtr2d φi=1B=⟨“ABC”⟩i
100 99 oveq1d φi=1B-˙A=⟨“ABC”⟩i-˙A
101 fveq2 i=1⟨“DEF”⟩i=⟨“DEF”⟩1
102 101 adantl φi=1⟨“DEF”⟩i=⟨“DEF”⟩1
103 56 adantr φi=1⟨“DEF”⟩1=E
104 102 103 eqtr2d φi=1E=⟨“DEF”⟩i
105 104 oveq1d φi=1E-˙D=⟨“DEF”⟩i-˙D
106 100 105 eqeq12d φi=1B-˙A=E-˙D⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D
107 99 oveq1d φi=1B-˙B=⟨“ABC”⟩i-˙B
108 104 oveq1d φi=1E-˙E=⟨“DEF”⟩i-˙E
109 107 108 eqeq12d φi=1B-˙B=E-˙E⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E
110 99 oveq1d φi=1B-˙C=⟨“ABC”⟩i-˙C
111 104 oveq1d φi=1E-˙F=⟨“DEF”⟩i-˙F
112 110 111 eqeq12d φi=1B-˙C=E-˙F⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
113 106 109 112 3anbi123d φi=1B-˙A=E-˙DB-˙B=E-˙EB-˙C=E-˙F⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
114 95 113 bitr4d φi=1j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩jB-˙A=E-˙DB-˙B=E-˙EB-˙C=E-˙F
115 74 adantr φi=2j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
116 fveq2 i=2⟨“ABC”⟩i=⟨“ABC”⟩2
117 116 adantl φi=2⟨“ABC”⟩i=⟨“ABC”⟩2
118 62 adantr φi=2⟨“ABC”⟩2=C
119 117 118 eqtr2d φi=2C=⟨“ABC”⟩i
120 119 oveq1d φi=2C-˙A=⟨“ABC”⟩i-˙A
121 fveq2 i=2⟨“DEF”⟩i=⟨“DEF”⟩2
122 121 adantl φi=2⟨“DEF”⟩i=⟨“DEF”⟩2
123 67 adantr φi=2⟨“DEF”⟩2=F
124 122 123 eqtr2d φi=2F=⟨“DEF”⟩i
125 124 oveq1d φi=2F-˙D=⟨“DEF”⟩i-˙D
126 120 125 eqeq12d φi=2C-˙A=F-˙D⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D
127 119 oveq1d φi=2C-˙B=⟨“ABC”⟩i-˙B
128 124 oveq1d φi=2F-˙E=⟨“DEF”⟩i-˙E
129 127 128 eqeq12d φi=2C-˙B=F-˙E⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E
130 119 oveq1d φi=2C-˙C=⟨“ABC”⟩i-˙C
131 124 oveq1d φi=2F-˙F=⟨“DEF”⟩i-˙F
132 130 131 eqeq12d φi=2C-˙C=F-˙F⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
133 126 129 132 3anbi123d φi=2C-˙A=F-˙DC-˙B=F-˙EC-˙C=F-˙F⟨“ABC”⟩i-˙A=⟨“DEF”⟩i-˙D⟨“ABC”⟩i-˙B=⟨“DEF”⟩i-˙E⟨“ABC”⟩i-˙C=⟨“DEF”⟩i-˙F
134 115 133 bitr4d φi=2j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩jC-˙A=F-˙DC-˙B=F-˙EC-˙C=F-˙F
135 94 114 134 71 72 73 raltpd φi012j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩jA-˙A=D-˙DA-˙B=D-˙EA-˙C=D-˙FB-˙A=E-˙DB-˙B=E-˙EB-˙C=E-˙FC-˙A=F-˙DC-˙B=F-˙EC-˙C=F-˙F
136 an33rean A-˙A=D-˙DA-˙B=D-˙EA-˙C=D-˙FB-˙A=E-˙DB-˙B=E-˙EB-˙C=E-˙FC-˙A=F-˙DC-˙B=F-˙EC-˙C=F-˙FA-˙A=D-˙DB-˙B=E-˙EC-˙C=F-˙FA-˙B=D-˙EB-˙A=E-˙DB-˙C=E-˙FC-˙B=F-˙EA-˙C=D-˙FC-˙A=F-˙D
137 eqid ItvG=ItvG
138 1 2 137 4 5 8 tgcgrtriv φA-˙A=D-˙D
139 1 2 137 4 6 9 tgcgrtriv φB-˙B=E-˙E
140 1 2 137 4 7 10 tgcgrtriv φC-˙C=F-˙F
141 138 139 140 3jca φA-˙A=D-˙DB-˙B=E-˙EC-˙C=F-˙F
142 141 biantrurd φA-˙B=D-˙EB-˙A=E-˙DB-˙C=E-˙FC-˙B=F-˙EA-˙C=D-˙FC-˙A=F-˙DA-˙A=D-˙DB-˙B=E-˙EC-˙C=F-˙FA-˙B=D-˙EB-˙A=E-˙DB-˙C=E-˙FC-˙B=F-˙EA-˙C=D-˙FC-˙A=F-˙D
143 simprl φA-˙B=D-˙EB-˙A=E-˙DA-˙B=D-˙E
144 simpr φA-˙B=D-˙EA-˙B=D-˙E
145 4 adantr φA-˙B=D-˙EG𝒢Tarski
146 5 adantr φA-˙B=D-˙EAP
147 6 adantr φA-˙B=D-˙EBP
148 8 adantr φA-˙B=D-˙EDP
149 9 adantr φA-˙B=D-˙EEP
150 1 2 137 145 146 147 148 149 144 tgcgrcomlr φA-˙B=D-˙EB-˙A=E-˙D
151 144 150 jca φA-˙B=D-˙EA-˙B=D-˙EB-˙A=E-˙D
152 143 151 impbida φA-˙B=D-˙EB-˙A=E-˙DA-˙B=D-˙E
153 simprl φB-˙C=E-˙FC-˙B=F-˙EB-˙C=E-˙F
154 simpr φB-˙C=E-˙FB-˙C=E-˙F
155 4 adantr φB-˙C=E-˙FG𝒢Tarski
156 6 adantr φB-˙C=E-˙FBP
157 7 adantr φB-˙C=E-˙FCP
158 9 adantr φB-˙C=E-˙FEP
159 10 adantr φB-˙C=E-˙FFP
160 1 2 137 155 156 157 158 159 154 tgcgrcomlr φB-˙C=E-˙FC-˙B=F-˙E
161 154 160 jca φB-˙C=E-˙FB-˙C=E-˙FC-˙B=F-˙E
162 153 161 impbida φB-˙C=E-˙FC-˙B=F-˙EB-˙C=E-˙F
163 simprr φA-˙C=D-˙FC-˙A=F-˙DC-˙A=F-˙D
164 4 adantr φC-˙A=F-˙DG𝒢Tarski
165 7 adantr φC-˙A=F-˙DCP
166 5 adantr φC-˙A=F-˙DAP
167 10 adantr φC-˙A=F-˙DFP
168 8 adantr φC-˙A=F-˙DDP
169 simpr φC-˙A=F-˙DC-˙A=F-˙D
170 1 2 137 164 165 166 167 168 169 tgcgrcomlr φC-˙A=F-˙DA-˙C=D-˙F
171 170 169 jca φC-˙A=F-˙DA-˙C=D-˙FC-˙A=F-˙D
172 163 171 impbida φA-˙C=D-˙FC-˙A=F-˙DC-˙A=F-˙D
173 152 162 172 3anbi123d φA-˙B=D-˙EB-˙A=E-˙DB-˙C=E-˙FC-˙B=F-˙EA-˙C=D-˙FC-˙A=F-˙DA-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D
174 142 173 bitr3d φA-˙A=D-˙DB-˙B=E-˙EC-˙C=F-˙FA-˙B=D-˙EB-˙A=E-˙DB-˙C=E-˙FC-˙B=F-˙EA-˙C=D-˙FC-˙A=F-˙DA-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D
175 136 174 bitrid φA-˙A=D-˙DA-˙B=D-˙EA-˙C=D-˙FB-˙A=E-˙DB-˙B=E-˙EB-˙C=E-˙FC-˙A=F-˙DC-˙B=F-˙EC-˙C=F-˙FA-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D
176 135 175 bitr2d φA-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙Di012j012⟨“ABC”⟩i-˙⟨“ABC”⟩j=⟨“DEF”⟩i-˙⟨“DEF”⟩j
177 22 37 176 3bitr4d φ⟨“ABC”⟩˙⟨“DEF”⟩A-˙B=D-˙EB-˙C=E-˙FC-˙A=F-˙D