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

Theorem axtg5seg 25581
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 25569 . . . . . . 7 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 3982 . . . . . . . 8 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 3981 . . . . . . . 8 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3761 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3784 . . . . . 6 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3750 . . . . 5 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . . 8 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . . 8 = (dist‘𝐺)
10 axtrkg.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25572 . . . . . . 7 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 484 . . . . . 6 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simpld 482 . . . . 5 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
147, 13syl 17 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
15 axtg5seg.1 . . . . 5 (𝜑𝑋𝑃)
16 axtg5seg.2 . . . . 5 (𝜑𝑌𝑃)
17 axtg5seg.3 . . . . 5 (𝜑𝑍𝑃)
18 neeq1 3005 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝑦𝑋𝑦))
19 oveq1 6799 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2019eleq2d 2836 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2118, 203anbi12d 1548 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22 oveq1 6799 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2322eqeq1d 2773 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑦) = (𝑎 𝑏)))
2423anbi1d 615 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐))))
25 oveq1 6799 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
2625eqeq1d 2773 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑢) = (𝑎 𝑣)))
2726anbi1d 615 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))
2824, 27anbi12d 616 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))))
2921, 28anbi12d 616 . . . . . . . . . 10 (𝑥 = 𝑋 → (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))))
3029imbi1d 330 . . . . . . . . 9 (𝑥 = 𝑋 → ((((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
3130ralbidv 3135 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
32312ralbidv 3138 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
33322ralbidv 3138 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
34 neeq2 3006 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝑦𝑋𝑌))
35 eleq1 2838 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3634, 353anbi12d 1548 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37 oveq2 6800 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
3837eqeq1d 2773 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝑎 𝑏)))
39 oveq1 6799 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
4039eqeq1d 2773 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑧) = (𝑏 𝑐)))
4138, 40anbi12d 616 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐))))
42 oveq1 6799 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
4342eqeq1d 2773 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑢) = (𝑏 𝑣)))
4443anbi2d 614 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))
4541, 44anbi12d 616 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
4636, 45anbi12d 616 . . . . . . . . . 10 (𝑦 = 𝑌 → (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
4746imbi1d 330 . . . . . . . . 9 (𝑦 = 𝑌 → ((((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
4847ralbidv 3135 . . . . . . . 8 (𝑦 = 𝑌 → (∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
49482ralbidv 3138 . . . . . . 7 (𝑦 = 𝑌 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
50492ralbidv 3138 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
51 oveq2 6800 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5251eleq2d 2836 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53523anbi2d 1552 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54 oveq2 6800 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (𝑌 𝑧) = (𝑌 𝑍))
5554eqeq1d 2773 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → ((𝑌 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝑏 𝑐)))
5655anbi2d 614 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
5756anbi1d 615 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
5853, 57anbi12d 616 . . . . . . . . . 10 (𝑧 = 𝑍 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
59 oveq1 6799 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
6059eqeq1d 2773 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑢) = (𝑐 𝑣)))
6158, 60imbi12d 333 . . . . . . . . 9 (𝑧 = 𝑍 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6261ralbidv 3135 . . . . . . . 8 (𝑧 = 𝑍 → (∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
63622ralbidv 3138 . . . . . . 7 (𝑧 = 𝑍 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
64632ralbidv 3138 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6533, 50, 64rspc3v 3475 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6615, 16, 17, 65syl3anc 1476 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6714, 66mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)))
68 axtg5seg.7 . . . 4 (𝜑𝑈𝑃)
69 axtg5seg.4 . . . 4 (𝜑𝐴𝑃)
70 axtg5seg.5 . . . 4 (𝜑𝐵𝑃)
71 oveq2 6800 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
7271eqeq1d 2773 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝑎 𝑣)))
73 oveq2 6800 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
7473eqeq1d 2773 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝑏 𝑣)))
7572, 74anbi12d 616 . . . . . . . . 9 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
7675anbi2d 614 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
7776anbi2d 614 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
78 oveq2 6800 . . . . . . . 8 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
7978eqeq1d 2773 . . . . . . 7 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝑐 𝑣)))
8077, 79imbi12d 333 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
81802ralbidv 3138 . . . . 5 (𝑢 = 𝑈 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
82 oveq1 6799 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
8382eleq2d 2836 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84833anbi3d 1553 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85 oveq1 6799 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
8685eqeq2d 2781 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑌) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝑏)))
8786anbi1d 615 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
88 oveq1 6799 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑣) = (𝐴 𝑣))
8988eqeq2d 2781 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑈) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑣)))
9089anbi1d 615 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
9187, 90anbi12d 616 . . . . . . . 8 (𝑎 = 𝐴 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
9284, 91anbi12d 616 . . . . . . 7 (𝑎 = 𝐴 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
9392imbi1d 330 . . . . . 6 (𝑎 = 𝐴 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
94932ralbidv 3138 . . . . 5 (𝑎 = 𝐴 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
95 eleq1 2838 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96953anbi3d 1553 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97 oveq2 6800 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
9897eqeq2d 2781 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑋 𝑌) = (𝐴 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝐵)))
99 oveq1 6799 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑐) = (𝐵 𝑐))
10099eqeq2d 2781 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑍) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝑐)))
10198, 100anbi12d 616 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐))))
102 oveq1 6799 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑣) = (𝐵 𝑣))
103102eqeq2d 2781 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑈) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑣)))
104103anbi2d 614 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))
105101, 104anbi12d 616 . . . . . . . 8 (𝑏 = 𝐵 → ((((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
10696, 105anbi12d 616 . . . . . . 7 (𝑏 = 𝐵 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
107106imbi1d 330 . . . . . 6 (𝑏 = 𝐵 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
1081072ralbidv 3138 . . . . 5 (𝑏 = 𝐵 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
10981, 94, 108rspc3v 3475 . . . 4 ((𝑈𝑃𝐴𝑃𝐵𝑃) → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11068, 69, 70, 109syl3anc 1476 . . 3 (𝜑 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11167, 110mpd 15 . 2 (𝜑 → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)))
112 axtg5seg.9 . . . 4 (𝜑𝑋𝑌)
113 axtg5seg.10 . . . 4 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
114 axtg5seg.11 . . . 4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
115112, 113, 1143jca 1122 . . 3 (𝜑 → (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116 axtg5seg.12 . . . 4 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
117 axtg5seg.13 . . . 4 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
118116, 117jca 501 . . 3 (𝜑 → ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)))
119 axtg5seg.14 . . . 4 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
120 axtg5seg.15 . . . 4 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
121119, 120jca 501 . . 3 (𝜑 → ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))
122115, 118, 121jca32 505 . 2 (𝜑 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
123 axtg5seg.6 . . 3 (𝜑𝐶𝑃)
124 axtg5seg.8 . . 3 (𝜑𝑉𝑃)
125 oveq2 6800 . . . . . . . 8 (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126125eleq2d 2836 . . . . . . 7 (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
1271263anbi3d 1553 . . . . . 6 (𝑐 = 𝐶 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128 oveq2 6800 . . . . . . . . 9 (𝑐 = 𝐶 → (𝐵 𝑐) = (𝐵 𝐶))
129128eqeq2d 2781 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑌 𝑍) = (𝐵 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝐶)))
130129anbi2d 614 . . . . . . 7 (𝑐 = 𝐶 → (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶))))
131130anbi1d 615 . . . . . 6 (𝑐 = 𝐶 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
132127, 131anbi12d 616 . . . . 5 (𝑐 = 𝐶 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
133 oveq1 6799 . . . . . 6 (𝑐 = 𝐶 → (𝑐 𝑣) = (𝐶 𝑣))
134133eqeq2d 2781 . . . . 5 (𝑐 = 𝐶 → ((𝑍 𝑈) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑣)))
135132, 134imbi12d 333 . . . 4 (𝑐 = 𝐶 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣))))
136 oveq2 6800 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐴 𝑣) = (𝐴 𝑉))
137136eqeq2d 2781 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝐴 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑉)))
138 oveq2 6800 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐵 𝑣) = (𝐵 𝑉))
139138eqeq2d 2781 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝐵 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑉)))
140137, 139anbi12d 616 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))
141140anbi2d 614 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
142141anbi2d 614 . . . . 5 (𝑣 = 𝑉 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))))
143 oveq2 6800 . . . . . 6 (𝑣 = 𝑉 → (𝐶 𝑣) = (𝐶 𝑉))
144143eqeq2d 2781 . . . . 5 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝐶 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑉)))
145142, 144imbi12d 333 . . . 4 (𝑣 = 𝑉 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
146135, 145rspc2v 3472 . . 3 ((𝐶𝑃𝑉𝑃) → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
147123, 124, 146syl2anc 573 . 2 (𝜑 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
148111, 122, 147mp2d 49 1 (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3o 1070  w3a 1071   = wceq 1631  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  [wsbc 3587  cdif 3720  cin 3722  {csn 4316  cfv 6029  (class class class)co 6792  cmpt2 6794  Basecbs 16060  distcds 16154  TarskiGcstrkg 25546  TarskiGCcstrkgc 25547  TarskiGBcstrkgb 25548  TarskiGCBcstrkgcb 25549  Itvcitv 25552  LineGclng 25553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5992  df-fv 6037  df-ov 6795  df-trkgcb 25566  df-trkg 25569
This theorem is referenced by:  tgcgrextend  25597  tgsegconeq  25598  tgifscgr  25620  tgfscgr  25680  tgbtwnconn1lem2  25685  tgbtwnconn1lem3  25686  miriso  25782  midexlem  25804  ragcgr  25819  footex  25830  lmiisolem  25905  f1otrg  25968  tg5segofs  31087
  Copyright terms: Public domain W3C validator