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

Theorem axtg5seg 26262
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 26250 . . . . . . 7 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 4159 . . . . . . . 8 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 4158 . . . . . . . 8 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3927 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3952 . . . . . 6 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3916 . . . . 5 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . . 8 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . . 8 = (dist‘𝐺)
10 axtrkg.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 26253 . . . . . . 7 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 500 . . . . . 6 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simpld 498 . . . . 5 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
147, 13syl 17 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)))
15 axtg5seg.1 . . . . 5 (𝜑𝑋𝑃)
16 axtg5seg.2 . . . . 5 (𝜑𝑌𝑃)
17 axtg5seg.3 . . . . 5 (𝜑𝑍𝑃)
18 neeq1 3052 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝑦𝑋𝑦))
19 oveq1 7146 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2019eleq2d 2878 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2118, 203anbi12d 1434 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
22 oveq1 7146 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2322eqeq1d 2803 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑦) = (𝑎 𝑏)))
2423anbi1d 632 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐))))
25 oveq1 7146 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
2625eqeq1d 2803 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑢) = (𝑎 𝑣)))
2726anbi1d 632 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))
2824, 27anbi12d 633 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))))
2921, 28anbi12d 633 . . . . . . . . . 10 (𝑥 = 𝑋 → (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))))))
3029imbi1d 345 . . . . . . . . 9 (𝑥 = 𝑋 → ((((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
3130ralbidv 3165 . . . . . . . 8 (𝑥 = 𝑋 → (∀𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
32312ralbidv 3167 . . . . . . 7 (𝑥 = 𝑋 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
33322ralbidv 3167 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
34 neeq2 3053 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝑦𝑋𝑌))
35 eleq1 2880 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3634, 353anbi12d 1434 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
37 oveq2 7147 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
3837eqeq1d 2803 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝑎 𝑏)))
39 oveq1 7146 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
4039eqeq1d 2803 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑧) = (𝑏 𝑐)))
4138, 40anbi12d 633 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐))))
42 oveq1 7146 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
4342eqeq1d 2803 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑢) = (𝑏 𝑣)))
4443anbi2d 631 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))
4541, 44anbi12d 633 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
4636, 45anbi12d 633 . . . . . . . . . 10 (𝑦 = 𝑌 → (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
4746imbi1d 345 . . . . . . . . 9 (𝑦 = 𝑌 → ((((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
4847ralbidv 3165 . . . . . . . 8 (𝑦 = 𝑌 → (∀𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
49482ralbidv 3167 . . . . . . 7 (𝑦 = 𝑌 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
50492ralbidv 3167 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑦𝑦 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣))))
51 oveq2 7147 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5251eleq2d 2878 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
53523anbi2d 1438 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐))))
54 oveq2 7147 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (𝑌 𝑧) = (𝑌 𝑍))
5554eqeq1d 2803 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → ((𝑌 𝑧) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝑏 𝑐)))
5655anbi2d 631 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
5756anbi1d 632 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))))
5853, 57anbi12d 633 . . . . . . . . . 10 (𝑧 = 𝑍 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))))))
59 oveq1 7146 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
6059eqeq1d 2803 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑢) = (𝑐 𝑣)))
6158, 60imbi12d 348 . . . . . . . . 9 (𝑧 = 𝑍 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6261ralbidv 3165 . . . . . . . 8 (𝑧 = 𝑍 → (∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
63622ralbidv 3167 . . . . . . 7 (𝑧 = 𝑍 → (∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
64632ralbidv 3167 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑧) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ↔ ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6533, 50, 64rspc3v 3587 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6615, 16, 17, 65syl3anc 1368 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣))))
6714, 66mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)))
68 axtg5seg.7 . . . 4 (𝜑𝑈𝑃)
69 axtg5seg.4 . . . 4 (𝜑𝐴𝑃)
70 axtg5seg.5 . . . 4 (𝜑𝐵𝑃)
71 oveq2 7147 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
7271eqeq1d 2803 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝑎 𝑣)))
73 oveq2 7147 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
7473eqeq1d 2803 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝑏 𝑣)))
7572, 74anbi12d 633 . . . . . . . . 9 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
7675anbi2d 631 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
7776anbi2d 631 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
78 oveq2 7147 . . . . . . . 8 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
7978eqeq1d 2803 . . . . . . 7 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝑐 𝑣)))
8077, 79imbi12d 348 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
81802ralbidv 3167 . . . . 5 (𝑢 = 𝑈 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
82 oveq1 7146 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎𝐼𝑐) = (𝐴𝐼𝑐))
8382eleq2d 2878 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑏 ∈ (𝑎𝐼𝑐) ↔ 𝑏 ∈ (𝐴𝐼𝑐)))
84833anbi3d 1439 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐))))
85 oveq1 7146 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
8685eqeq2d 2812 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑌) = (𝑎 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝑏)))
8786anbi1d 632 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐))))
88 oveq1 7146 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑎 𝑣) = (𝐴 𝑣))
8988eqeq2d 2812 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝑋 𝑈) = (𝑎 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑣)))
9089anbi1d 632 . . . . . . . . 9 (𝑎 = 𝐴 → (((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))
9187, 90anbi12d 633 . . . . . . . 8 (𝑎 = 𝐴 → ((((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))))
9284, 91anbi12d 633 . . . . . . 7 (𝑎 = 𝐴 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))))))
9392imbi1d 345 . . . . . 6 (𝑎 = 𝐴 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
94932ralbidv 3167 . . . . 5 (𝑎 = 𝐴 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝑎 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
95 eleq1 2880 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝑐)))
96953anbi3d 1439 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐))))
97 oveq2 7147 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
9897eqeq2d 2812 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑋 𝑌) = (𝐴 𝑏) ↔ (𝑋 𝑌) = (𝐴 𝐵)))
99 oveq1 7146 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑐) = (𝐵 𝑐))
10099eqeq2d 2812 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑍) = (𝑏 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝑐)))
10198, 100anbi12d 633 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐))))
102 oveq1 7146 . . . . . . . . . . 11 (𝑏 = 𝐵 → (𝑏 𝑣) = (𝐵 𝑣))
103102eqeq2d 2812 . . . . . . . . . 10 (𝑏 = 𝐵 → ((𝑌 𝑈) = (𝑏 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑣)))
104103anbi2d 631 . . . . . . . . 9 (𝑏 = 𝐵 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))
105101, 104anbi12d 633 . . . . . . . 8 (𝑏 = 𝐵 → ((((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
10696, 105anbi12d 633 . . . . . . 7 (𝑏 = 𝐵 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
107106imbi1d 345 . . . . . 6 (𝑏 = 𝐵 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
1081072ralbidv 3167 . . . . 5 (𝑏 = 𝐵 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝑏 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
10981, 94, 108rspc3v 3587 . . . 4 ((𝑈𝑃𝐴𝑃𝐵𝑃) → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11068, 69, 70, 109syl3anc 1368 . . 3 (𝜑 → (∀𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝑎 𝑏) ∧ (𝑌 𝑍) = (𝑏 𝑐)) ∧ ((𝑋 𝑢) = (𝑎 𝑣) ∧ (𝑌 𝑢) = (𝑏 𝑣)))) → (𝑍 𝑢) = (𝑐 𝑣)) → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣))))
11167, 110mpd 15 . 2 (𝜑 → ∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)))
112 axtg5seg.9 . . . 4 (𝜑𝑋𝑌)
113 axtg5seg.10 . . . 4 (𝜑𝑌 ∈ (𝑋𝐼𝑍))
114 axtg5seg.11 . . . 4 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
115112, 113, 1143jca 1125 . . 3 (𝜑 → (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)))
116 axtg5seg.12 . . . 4 (𝜑 → (𝑋 𝑌) = (𝐴 𝐵))
117 axtg5seg.13 . . . 4 (𝜑 → (𝑌 𝑍) = (𝐵 𝐶))
118116, 117jca 515 . . 3 (𝜑 → ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)))
119 axtg5seg.14 . . . 4 (𝜑 → (𝑋 𝑈) = (𝐴 𝑉))
120 axtg5seg.15 . . . 4 (𝜑 → (𝑌 𝑈) = (𝐵 𝑉))
121119, 120jca 515 . . 3 (𝜑 → ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))
122115, 118, 121jca32 519 . 2 (𝜑 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
123 axtg5seg.6 . . 3 (𝜑𝐶𝑃)
124 axtg5seg.8 . . 3 (𝜑𝑉𝑃)
125 oveq2 7147 . . . . . . . 8 (𝑐 = 𝐶 → (𝐴𝐼𝑐) = (𝐴𝐼𝐶))
126125eleq2d 2878 . . . . . . 7 (𝑐 = 𝐶 → (𝐵 ∈ (𝐴𝐼𝑐) ↔ 𝐵 ∈ (𝐴𝐼𝐶)))
1271263anbi3d 1439 . . . . . 6 (𝑐 = 𝐶 → ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ↔ (𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶))))
128 oveq2 7147 . . . . . . . . 9 (𝑐 = 𝐶 → (𝐵 𝑐) = (𝐵 𝐶))
129128eqeq2d 2812 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑌 𝑍) = (𝐵 𝑐) ↔ (𝑌 𝑍) = (𝐵 𝐶)))
130129anbi2d 631 . . . . . . 7 (𝑐 = 𝐶 → (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ↔ ((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶))))
131130anbi1d 632 . . . . . 6 (𝑐 = 𝐶 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))))
132127, 131anbi12d 633 . . . . 5 (𝑐 = 𝐶 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))))))
133 oveq1 7146 . . . . . 6 (𝑐 = 𝐶 → (𝑐 𝑣) = (𝐶 𝑣))
134133eqeq2d 2812 . . . . 5 (𝑐 = 𝐶 → ((𝑍 𝑈) = (𝑐 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑣)))
135132, 134imbi12d 348 . . . 4 (𝑐 = 𝐶 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣))))
136 oveq2 7147 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐴 𝑣) = (𝐴 𝑉))
137136eqeq2d 2812 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝐴 𝑣) ↔ (𝑋 𝑈) = (𝐴 𝑉)))
138 oveq2 7147 . . . . . . . . 9 (𝑣 = 𝑉 → (𝐵 𝑣) = (𝐵 𝑉))
139138eqeq2d 2812 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝐵 𝑣) ↔ (𝑌 𝑈) = (𝐵 𝑉)))
140137, 139anbi12d 633 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)) ↔ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))
141140anbi2d 631 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣))) ↔ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))))
142141anbi2d 631 . . . . 5 (𝑣 = 𝑉 → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) ↔ ((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉))))))
143 oveq2 7147 . . . . . 6 (𝑣 = 𝑉 → (𝐶 𝑣) = (𝐶 𝑉))
144143eqeq2d 2812 . . . . 5 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝐶 𝑣) ↔ (𝑍 𝑈) = (𝐶 𝑉)))
145142, 144imbi12d 348 . . . 4 (𝑣 = 𝑉 → ((((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝐶 𝑣)) ↔ (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
146135, 145rspc2v 3584 . . 3 ((𝐶𝑃𝑉𝑃) → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
147123, 124, 146syl2anc 587 . 2 (𝜑 → (∀𝑐𝑃𝑣𝑃 (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝑐)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝑐)) ∧ ((𝑋 𝑈) = (𝐴 𝑣) ∧ (𝑌 𝑈) = (𝐵 𝑣)))) → (𝑍 𝑈) = (𝑐 𝑣)) → (((𝑋𝑌𝑌 ∈ (𝑋𝐼𝑍) ∧ 𝐵 ∈ (𝐴𝐼𝐶)) ∧ (((𝑋 𝑌) = (𝐴 𝐵) ∧ (𝑌 𝑍) = (𝐵 𝐶)) ∧ ((𝑋 𝑈) = (𝐴 𝑉) ∧ (𝑌 𝑈) = (𝐵 𝑉)))) → (𝑍 𝑈) = (𝐶 𝑉))))
148111, 122, 147mp2d 49 1 (𝜑 → (𝑍 𝑈) = (𝐶 𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3o 1083  w3a 1084   = wceq 1538  wcel 2112  {cab 2779  wne 2990  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  [wsbc 3723  cdif 3881  cin 3883  {csn 4528  cfv 6328  (class class class)co 7139  cmpo 7141  Basecbs 16478  distcds 16569  TarskiGcstrkg 26227  TarskiGCcstrkgc 26228  TarskiGBcstrkgb 26229  TarskiGCBcstrkgcb 26230  Itvcitv 26233  LineGclng 26234
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-trkgcb 26247  df-trkg 26250
This theorem is referenced by:  tgcgrextend  26282  tgsegconeq  26283  tgifscgr  26305  tgfscgr  26365  tgbtwnconn1lem2  26370  tgbtwnconn1lem3  26371  miriso  26467  midexlem  26489  ragcgr  26504  footexALT  26515  footexlem1  26516  footexlem2  26517  lmiisolem  26593  f1otrg  26668  tg5segofs  32052
  Copyright terms: Public domain W3C validator