Metamath Proof Explorer


Theorem tglngval

Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)

Ref Expression
Hypotheses tglngval.p 𝑃 = ( Base ‘ 𝐺 )
tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ( 𝜑𝐺 ∈ TarskiG )
tglngval.x ( 𝜑𝑋𝑃 )
tglngval.y ( 𝜑𝑌𝑃 )
tglngval.z ( 𝜑𝑋𝑌 )
Assertion tglngval ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )

Proof

Step Hyp Ref Expression
1 tglngval.p 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ( 𝜑𝐺 ∈ TarskiG )
5 tglngval.x ( 𝜑𝑋𝑃 )
6 tglngval.y ( 𝜑𝑌𝑃 )
7 tglngval.z ( 𝜑𝑋𝑌 )
8 1 2 3 tglng ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
9 4 8 syl ( 𝜑𝐿 = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
10 9 oveqd ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) )
11 7 necomd ( 𝜑𝑌𝑋 )
12 eldifsn ( 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) ↔ ( 𝑌𝑃𝑌𝑋 ) )
13 6 11 12 sylanbrc ( 𝜑𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
14 1 fvexi 𝑃 ∈ V
15 14 rabex { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V
16 15 a1i ( 𝜑 → { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V )
17 oveq12 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑋 𝐼 𝑌 ) )
18 17 eleq2d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ) )
19 simpl ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
20 simpr ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
21 20 oveq2d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑧 𝐼 𝑦 ) = ( 𝑧 𝐼 𝑌 ) )
22 19 21 eleq12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ) )
23 19 oveq1d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
24 20 23 eleq12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
25 18 22 24 3orbi123d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) ) )
26 25 rabbidv ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
27 sneq ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
28 27 difeq2d ( 𝑥 = 𝑋 → ( 𝑃 ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑋 } ) )
29 eqid ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
30 26 28 29 ovmpox ( ( 𝑋𝑃𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) ∧ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } ∈ V ) → ( 𝑋 ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
31 5 13 16 30 syl3anc ( 𝜑 → ( 𝑋 ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) 𝑌 ) = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )
32 10 31 eqtrd ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑧 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) } )