Metamath Proof Explorer

Theorem angmgmaddrid

Description: The right identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmgmadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmgmadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
angmgmadd.d ⊢ − = ( dist ‘ 𝐺 )
angmgmadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmgmadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
angmgmadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
angmgmadd.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
angmgmaddlid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
angmgmaddlid.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
angmgmaddlid.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
Assertion angmgmaddrid ( 𝜑 → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )

Proof

Step Hyp Ref Expression
1 angmgmadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmgmadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmgmadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmgmadd.d ⊢ − = ( dist ‘ 𝐺 )
5 angmgmadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmgmadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmgmadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 angmgmadd.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
9 angmgmaddlid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 angmgmaddlid.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
11 angmgmaddlid.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
12 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
13 12 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) )
14 7 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝐺 ∈ TarskiG )
15 14 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝐺 ∈ TarskiG )
16 9 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑋 ∈ 𝑃 )
17 16 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑋 ∈ 𝑃 )
18 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
19 18 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑌 ∈ 𝑃 )
20 19 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ∈ 𝑃 )
21 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑢 ∈ 𝑃 )
22 21 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ∈ 𝑃 )
23 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑣 ∈ 𝑃 )
24 23 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ∈ 𝑃 )
25 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑤 ∈ 𝑃 )
26 25 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑤 ∈ 𝑃 )
27 10 eldifsnbd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
28 27 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
29 28 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑋 ≠ 𝑌 )
30 29 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑋 ≠ 𝑌 )
31 27 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑌 ≠ 𝑋 )
32 31 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ≠ 𝑋 )
33 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑢 ≠ 𝑣 )
34 33 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ≠ 𝑣 )
35 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ≠ 𝑤 )
36 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) )
37 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑡 ∈ 𝑃 )
38 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
39 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
40 1 3 38 37 17 20 15 39 hlcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑡 )
41 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 )
42 1 3 38 26 22 24 15 41 hlcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 )
43 1 5 38 15 40 42 20 24 zerocgra ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ⟨“ 𝑋 𝑌 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
44 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) )
45 1 2 3 4 5 6 15 17 20 17 22 24 26 30 32 34 35 8 36 37 43 44 angmgmaddov2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑋 𝑌 𝑡 ”⟩ )
46 13 45 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑋 𝑌 𝑡 ”⟩ )
47 46 43 eqbrtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
48 47 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
49 18 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑌 ∈ 𝑃 )
50 23 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑣 ∈ 𝑃 )
51 21 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑢 ∈ 𝑃 )
52 14 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝐺 ∈ TarskiG )
53 16 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑋 ∈ 𝑃 )
54 28 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑋 ≠ 𝑌 )
55 33 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑢 ≠ 𝑣 )
56 55 necomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → 𝑣 ≠ 𝑢 )
57 1 3 38 49 50 51 52 53 4 54 56 hlcgrex ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) )
58 48 57 r19.29a ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
59 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
60 59 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) )
61 14 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → 𝐺 ∈ TarskiG )
62 61 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝐺 ∈ TarskiG )
63 16 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → 𝑋 ∈ 𝑃 )
64 63 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑋 ∈ 𝑃 )
65 18 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → 𝑌 ∈ 𝑃 )
66 65 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ∈ 𝑃 )
67 21 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → 𝑢 ∈ 𝑃 )
68 67 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ∈ 𝑃 )
69 23 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → 𝑣 ∈ 𝑃 )
70 69 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ∈ 𝑃 )
71 25 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑤 ∈ 𝑃 )
72 29 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑋 ≠ 𝑌 )
73 72 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ≠ 𝑋 )
74 33 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ≠ 𝑣 )
75 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ≠ 𝑤 )
76 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) )
77 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑡 ∈ 𝑃 )
78 5 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
79 78 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
80 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) )
81 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) )
82 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) )
83 82 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝑣 − 𝑢 ) = ( 𝑌 − 𝑡 ) )
84 74 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑣 ≠ 𝑢 )
85 1 4 3 62 70 68 66 77 83 84 tgcgrneq ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑌 ≠ 𝑡 )
86 85 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑡 ≠ 𝑌 )
87 75 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → 𝑤 ≠ 𝑣 )
88 1 3 4 62 64 66 77 68 70 71 80 81 72 86 74 87 flatcgra ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ⟨“ 𝑋 𝑌 𝑡 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
89 79 88 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ⟨“ 𝑋 𝑌 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
90 1 2 3 4 5 6 62 64 66 64 68 70 71 72 73 74 75 8 76 77 89 82 angmgmaddov2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑋 𝑌 𝑡 ”⟩ )
91 60 90 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑋 𝑌 𝑡 ”⟩ )
92 91 89 eqbrtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
93 92 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
94 1 4 3 61 63 65 69 67 axtgsegcon ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → ∃ 𝑡 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑡 ) ∧ ( 𝑌 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) )
95 93 94 r19.29a ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
96 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) )
97 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑣 ≠ 𝑤 )
98 1 3 6 14 21 23 25 33 96 97 lnrot2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑤 ∈ ( 𝑢 𝐿 𝑣 ) )
99 1 3 38 21 23 25 14 16 6 98 lnhl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → ( 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑢 ∨ 𝑣 ∈ ( 𝑢 𝐼 𝑤 ) ) )
100 58 95 99 mpjaodan ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
101 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
102 101 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) )
103 7 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝐺 ∈ TarskiG )
104 103 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝐺 ∈ TarskiG )
105 9 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑋 ∈ 𝑃 )
106 105 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ∈ 𝑃 )
107 18 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑌 ∈ 𝑃 )
108 107 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ∈ 𝑃 )
109 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑢 ∈ 𝑃 )
110 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑣 ∈ 𝑃 )
111 110 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ∈ 𝑃 )
112 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑤 ∈ 𝑃 )
113 112 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑤 ∈ 𝑃 )
114 28 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ≠ 𝑌 )
115 27 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑌 ≠ 𝑋 )
116 115 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ≠ 𝑋 )
117 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑢 ≠ 𝑣 )
118 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ≠ 𝑤 )
119 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) )
120 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ∈ 𝑃 )
121 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 )
122 1 3 38 120 113 111 104 121 hlcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑡 )
123 1 3 38 106 106 108 104 114 hlid ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
124 1 5 38 104 122 123 111 108 zerocgra ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑋 ”⟩ )
125 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) )
126 1 3 38 113 120 111 104 6 122 hlln ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑤 ∈ ( 𝑡 𝐿 𝑣 ) )
127 1 6 3 104 120 111 126 tglngne ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ≠ 𝑣 )
128 1 3 6 104 111 113 120 118 126 127 lnrot1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ∈ ( 𝑣 𝐿 𝑤 ) )
129 1 4 3 104 120 109 tgbtwntriv1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ∈ ( 𝑡 𝐼 𝑢 ) )
130 128 129 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ∈ ( ( 𝑣 𝐿 𝑤 ) ∩ ( 𝑡 𝐼 𝑢 ) ) )
131 130 ne0d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ( 𝑣 𝐿 𝑤 ) ∩ ( 𝑡 𝐼 𝑢 ) ) ≠ ∅ )
132 1 2 3 4 5 6 104 106 108 106 109 111 113 114 116 117 118 8 119 120 124 125 131 angmgmaddov1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑢 𝑣 𝑤 ”⟩ + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
133 102 132 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
134 78 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
135 127 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ≠ 𝑡 )
136 1 3 104 38 109 111 120 117 135 cgraid ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
137 1 3 38 104 109 111 120 109 111 120 136 113 122 cgrahl2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
138 134 137 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
139 133 138 eqbrtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
140 139 anasss ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
141 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑣 ≠ 𝑤 )
142 141 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → 𝑤 ≠ 𝑣 )
143 1 3 38 110 107 105 103 112 4 142 115 hlcgrex ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) )
144 140 143 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑢 ∈ ( 𝑣 𝐿 𝑤 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
145 100 144 pm2.61dan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
146 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
147 145 146 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )
148 147 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )
149 148 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )
150 149 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )
151 1 fvexi ⊢ 𝑃 ∈ V
152 151 2 11 elcgrabasi ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
153 150 152 r19.29vva ⊢ ( 𝜑 → ( 𝐸 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝐸 )