MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtg5seg Structured version   Visualization version   GIF version

Theorem axtg5seg 27407
Description: Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles 𝑋𝑍𝑈 and 𝐴𝐶𝑉, a point 𝑌 on 𝑋𝑍, and a point 𝐵 on 𝐴𝐶. If all corresponding line segments except for 𝑍𝑈 and 𝐶𝑉 are congruent ( i.e., 𝑋𝑌 𝐴𝐵, 𝑌𝑍 𝐵𝐶, 𝑋𝑈 𝐴𝑉, and 𝑌𝑈 𝐵𝑉), then 𝑍𝑈 and 𝐶𝑉 are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p 𝑃 = (Base‘𝐺)
axtrkg.d = (dist‘𝐺)
axtrkg.i 𝐼 = (Itv‘𝐺)
axtrkg.g (𝜑𝐺 ∈ TarskiG)
axtg5seg.1 (𝜑𝑋𝑃)
axtg5seg.2 (𝜑𝑌𝑃)
axtg5seg.3 (𝜑𝑍𝑃)
axtg5seg.4 (𝜑𝐴𝑃)
axtg5seg.5 (𝜑𝐵𝑃)
axtg5seg.6 (𝜑𝐶𝑃)
axtg5seg.7 (𝜑𝑈𝑃)
axtg5seg.8 (𝜑𝑉𝑃)
axtg5seg.9 (𝜑𝑋𝑌)
axtg5seg.10 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
axtg5seg.11 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
axtg5seg.12 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
axtg5seg.13 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
axtg5seg.14 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
axtg5seg.15 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
Assertion
Ref Expression
axtg5seg (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))

Proof of Theorem axtg5seg
Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 27395 . . . . . . 7 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 4189 . . . . . . . 8 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 4188 . . . . . . . 8 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3953 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3978 . . . . . 6 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
75, 6sselid 3942 . . . . 5 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . . 8 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . . 8 = (dist‘𝐺)
10 axtrkg.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 27398 . . . . . . 7 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 497 . . . . . 6 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simpld 495 . . . . 5 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
147, 13syl 17 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
15 axtg5seg.1 . . . . 5 (𝜑𝑋𝑃)
16 axtg5seg.2 . . . . 5 (𝜑𝑌𝑃)
17 axtg5seg.3 . . . . 5 (𝜑𝑍𝑃)
18 neeq1 3006 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝑦𝑋𝑦))
19 oveq1 7364 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2019eleq2d 2823 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2118, 203anbi12d 1437 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22 oveq1 7364 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2322eqeq1d 2738 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑦) = (𝑎 𝑏)))
2423anbi1d 630 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐))))
25 oveq1 7364 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
2625eqeq1d 2738 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑢) = (𝑎 𝑣)))
2726anbi1d 630 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))
2824, 27anbi12d 631 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))))
2921, 28anbi12d 631 . . . . . . . . . 10 (𝑥 = 𝑋 → (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))))
3029imbi1d 341 . . . . . . . . 9 (𝑥 = 𝑋 → ((((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
3130ralbidv 3174 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
32312ralbidv 3212 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
33322ralbidv 3212 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
34 neeq2 3007 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝑦𝑋𝑌))
35 eleq1 2825 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3634, 353anbi12d 1437 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37 oveq2 7365 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
3837eqeq1d 2738 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝑎 𝑏)))
39 oveq1 7364 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
4039eqeq1d 2738 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑧) = (𝑏 𝑐)))
4138, 40anbi12d 631 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐))))
42 oveq1 7364 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
4342eqeq1d 2738 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑢) = (𝑏 𝑣)))
4443anbi2d 629 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))
4541, 44anbi12d 631 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
4636, 45anbi12d 631 . . . . . . . . . 10 (𝑦 = 𝑌 → (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
4746imbi1d 341 . . . . . . . . 9 (𝑦 = 𝑌 → ((((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
4847ralbidv 3174 . . . . . . . 8 (𝑦 = 𝑌 → (∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
49482ralbidv 3212 . . . . . . 7 (𝑦 = 𝑌 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
50492ralbidv 3212 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
51 oveq2 7365 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5251eleq2d 2823 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53523anbi2d 1441 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54 oveq2 7365 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (𝑌 𝑧) = (𝑌 𝑍))
5554eqeq1d 2738 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → ((𝑌 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝑏 𝑐)))
5655anbi2d 629 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
5756anbi1d 630 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
5853, 57anbi12d 631 . . . . . . . . . 10 (𝑧 = 𝑍 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
59 oveq1 7364 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
6059eqeq1d 2738 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑢) = (𝑐 𝑣)))
6158, 60imbi12d 344 . . . . . . . . 9 (𝑧 = 𝑍 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6261ralbidv 3174 . . . . . . . 8 (𝑧 = 𝑍 → (∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
63622ralbidv 3212 . . . . . . 7 (𝑧 = 𝑍 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
64632ralbidv 3212 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6533, 50, 64rspc3v 3593 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6615, 16, 17, 65syl3anc 1371 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6714, 66mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)))
68 axtg5seg.7 . . . 4 (𝜑𝑈𝑃)
69 axtg5seg.4 . . . 4 (𝜑𝐴𝑃)
70 axtg5seg.5 . . . 4 (𝜑𝐵𝑃)
71 oveq2 7365 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
7271eqeq1d 2738 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝑎 𝑣)))
73 oveq2 7365 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
7473eqeq1d 2738 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝑏 𝑣)))
7572, 74anbi12d 631 . . . . . . . . 9 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
7675anbi2d 629 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
7776anbi2d 629 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
78 oveq2 7365 . . . . . . . 8 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
7978eqeq1d 2738 . . . . . . 7 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝑐 𝑣)))
8077, 79imbi12d 344 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
81802ralbidv 3212 . . . . 5 (𝑢 = 𝑈 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
82 oveq1 7364 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
8382eleq2d 2823 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84833anbi3d 1442 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85 oveq1 7364 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
8685eqeq2d 2747 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑌) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝑏)))
8786anbi1d 630 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
88 oveq1 7364 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑣) = (𝐴 𝑣))
8988eqeq2d 2747 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑈) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑣)))
9089anbi1d 630 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
9187, 90anbi12d 631 . . . . . . . 8 (𝑎 = 𝐴 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
9284, 91anbi12d 631 . . . . . . 7 (𝑎 = 𝐴 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
9392imbi1d 341 . . . . . 6 (𝑎 = 𝐴 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
94932ralbidv 3212 . . . . 5 (𝑎 = 𝐴 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
95 eleq1 2825 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96953anbi3d 1442 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97 oveq2 7365 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
9897eqeq2d 2747 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑋 𝑌) = (𝐴 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝐵)))
99 oveq1 7364 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑐) = (𝐵 𝑐))
10099eqeq2d 2747 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑍) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝑐)))
10198, 100anbi12d 631 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐))))
102 oveq1 7364 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑣) = (𝐵 𝑣))
103102eqeq2d 2747 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑈) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑣)))
104103anbi2d 629 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))
105101, 104anbi12d 631 . . . . . . . 8 (𝑏 = 𝐵 → ((((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
10696, 105anbi12d 631 . . . . . . 7 (𝑏 = 𝐵 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
107106imbi1d 341 . . . . . 6 (𝑏 = 𝐵 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
1081072ralbidv 3212 . . . . 5 (𝑏 = 𝐵 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
10981, 94, 108rspc3v 3593 . . . 4 ((𝑈𝑃𝐴𝑃𝐵𝑃) → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11068, 69, 70, 109syl3anc 1371 . . 3 (𝜑 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11167, 110mpd 15 . 2 (𝜑 → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)))
112 axtg5seg.9 . . . 4 (𝜑𝑋𝑌)
113 axtg5seg.10 . . . 4 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
114 axtg5seg.11 . . . 4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
115112, 113, 1143jca 1128 . . 3 (𝜑 → (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116 axtg5seg.12 . . . 4 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
117 axtg5seg.13 . . . 4 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
118116, 117jca 512 . . 3 (𝜑 → ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)))
119 axtg5seg.14 . . . 4 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
120 axtg5seg.15 . . . 4 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
121119, 120jca 512 . . 3 (𝜑 → ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))
122115, 118, 121jca32 516 . 2 (𝜑 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
123 axtg5seg.6 . . 3 (𝜑𝐶𝑃)
124 axtg5seg.8 . . 3 (𝜑𝑉𝑃)
125 oveq2 7365 . . . . . . . 8 (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126125eleq2d 2823 . . . . . . 7 (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
1271263anbi3d 1442 . . . . . 6 (𝑐 = 𝐶 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128 oveq2 7365 . . . . . . . . 9 (𝑐 = 𝐶 → (𝐵 𝑐) = (𝐵 𝐶))
129128eqeq2d 2747 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑌 𝑍) = (𝐵 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝐶)))
130129anbi2d 629 . . . . . . 7 (𝑐 = 𝐶 → (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶))))
131130anbi1d 630 . . . . . 6 (𝑐 = 𝐶 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
132127, 131anbi12d 631 . . . . 5 (𝑐 = 𝐶 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
133 oveq1 7364 . . . . . 6 (𝑐 = 𝐶 → (𝑐 𝑣) = (𝐶 𝑣))
134133eqeq2d 2747 . . . . 5 (𝑐 = 𝐶 → ((𝑍 𝑈) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑣)))
135132, 134imbi12d 344 . . . 4 (𝑐 = 𝐶 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣))))
136 oveq2 7365 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐴 𝑣) = (𝐴 𝑉))
137136eqeq2d 2747 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝐴 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑉)))
138 oveq2 7365 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐵 𝑣) = (𝐵 𝑉))
139138eqeq2d 2747 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝐵 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑉)))
140137, 139anbi12d 631 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))
141140anbi2d 629 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
142141anbi2d 629 . . . . 5 (𝑣 = 𝑉 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))))
143 oveq2 7365 . . . . . 6 (𝑣 = 𝑉 → (𝐶 𝑣) = (𝐶 𝑉))
144143eqeq2d 2747 . . . . 5 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝐶 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑉)))
145142, 144imbi12d 344 . . . 4 (𝑣 = 𝑉 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
146135, 145rspc2v 3590 . . 3 ((𝐶𝑃𝑉𝑃) → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
147123, 124, 146syl2anc 584 . 2 (𝜑 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
148111, 122, 147mp2d 49 1 (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  cin 3909  {csn 4586  cfv 6496  (class class class)co 7357  cmpo 7359  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  TarskiGCcstrkgc 27370  TarskiGBcstrkgb 27371  TarskiGCBcstrkgcb 27372  Itvcitv 27375  LineGclng 27376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-trkgcb 27392  df-trkg 27395
This theorem is referenced by:  tgcgrextend  27427  tgsegconeq  27428  tgifscgr  27450  tgfscgr  27510  tgbtwnconn1lem2  27515  tgbtwnconn1lem3  27516  miriso  27612  midexlem  27634  ragcgr  27649  footexALT  27660  footexlem1  27661  footexlem2  27662  lmiisolem  27738  f1otrg  27813  tg5segofs  33286
  Copyright terms: Public domain W3C validator