Metamath Proof Explorer


Theorem istrkgl

Description: Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p 𝑃 = ( Base ‘ 𝐺 )
istrkg.d = ( dist ‘ 𝐺 )
istrkg.i 𝐼 = ( Itv ‘ 𝐺 )
Assertion istrkgl ( 𝐺 ∈ { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ↔ ( 𝐺 ∈ V ∧ ( LineG ‘ 𝐺 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 𝑃 = ( Base ‘ 𝐺 )
2 istrkg.d = ( dist ‘ 𝐺 )
3 istrkg.i 𝐼 = ( Itv ‘ 𝐺 )
4 simpl ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5 4 difeq1d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑝 ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑥 } ) )
6 simpr ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
7 6 oveqd ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑦 ) = ( 𝑥 𝐼 𝑦 ) )
8 7 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ) )
9 6 oveqd ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑧 𝑖 𝑦 ) = ( 𝑧 𝐼 𝑦 ) )
10 9 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) )
11 6 oveqd ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑧 ) = ( 𝑥 𝐼 𝑧 ) )
12 11 eleq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
13 8 10 12 3orbi123d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
14 4 13 rabeqbidv ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } = { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
15 4 5 14 mpoeq123dv ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
16 15 eqeq2d ( ( 𝑝 = 𝑃𝑖 = 𝐼 ) → ( ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ↔ ( LineG ‘ 𝑓 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
17 1 3 16 sbcie2s ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ↔ ( LineG ‘ 𝑓 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
18 fveqeq2 ( 𝑓 = 𝐺 → ( ( LineG ‘ 𝑓 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ( LineG ‘ 𝐺 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
19 17 18 bitrd ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) ↔ ( LineG ‘ 𝐺 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
20 eqid { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } = { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) }
21 19 20 elab4g ( 𝐺 ∈ { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ↔ ( 𝐺 ∈ V ∧ ( LineG ‘ 𝐺 ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )