Metamath Proof Explorer

Theorem plngrotlem3

Description: Lemma for plngrot . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
plngrot.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
plngrot.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
plngrot.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
plngrot.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
plngrotlem3.1 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
Assertion plngrotlem3 ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 plngrot.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
7 plngrot.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 plngrot.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
9 plngrot.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
10 plngrotlem3.1 ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑌 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
11 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝐺 ∈ TarskiG )
12 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
13 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑌 ∈ 𝑃 )
14 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
15 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑋 ≠ 𝑌 )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑤 ∈ 𝑃 )
17 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) )
18 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → 𝑌 ≠ 𝑤 )
19 1 2 3 4 11 12 13 14 15 10 16 17 18 plngrotlem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ) ∧ 𝑌 ≠ 𝑤 ) → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
20 19 anasss ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ∧ 𝑌 ≠ 𝑤 ) ) → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )
21 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
22 8 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
23 1 fvexi ⊢ 𝑃 ∈ V
24 23 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
25 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
26 24 25 7 9 nehash2 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
27 1 21 2 5 22 7 26 tgbtwndiff ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑃 ( 𝑌 ∈ ( 𝑍 𝐼 𝑤 ) ∧ 𝑌 ≠ 𝑤 ) )
28 20 27 r19.29a ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑍 ) ⊆ ( ( 𝑍 𝐿 𝑌 ) 𝐸 𝑋 ) )