Metamath Proof Explorer

Theorem angmgmaddlid

Description: The left 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 angmgmaddlid ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )

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-6r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
13 12 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) )
14 7 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝐺 ∈ TarskiG )
15 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑢 ∈ 𝑃 )
16 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ∈ 𝑃 )
17 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑤 ∈ 𝑃 )
18 9 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ∈ 𝑃 )
19 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
20 19 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ∈ 𝑃 )
21 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑢 ≠ 𝑣 )
22 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ≠ 𝑤 )
23 10 eldifsnbd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
24 23 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
25 24 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ≠ 𝑌 )
26 25 necomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑌 ≠ 𝑋 )
27 1 3 6 14 20 18 26 tglinerflx2 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) )
28 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ∈ 𝑃 )
29 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
30 simplr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 )
31 1 3 29 28 17 16 14 30 hlcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑡 )
32 1 3 29 18 15 20 14 25 hlid ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑋 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 )
33 1 5 29 14 31 32 16 20 zerocgra ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑋 ”⟩ )
34 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) )
35 1 2 3 4 5 6 14 15 16 17 18 20 18 21 22 25 26 8 27 28 33 34 angmgmaddov2 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
36 13 35 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
37 5 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
38 37 a1i ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
39 34 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( 𝑌 − 𝑋 ) = ( 𝑣 − 𝑡 ) )
40 1 4 3 14 20 18 16 28 39 26 tgcgrneq ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → 𝑣 ≠ 𝑡 )
41 1 3 14 29 15 16 28 21 40 cgraid ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
42 1 3 29 14 15 16 28 15 16 28 41 17 31 cgrahl2 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
43 38 42 breqdi ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
44 36 43 eqbrtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ) ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
45 44 anasss ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
46 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑣 ∈ 𝑃 )
47 19 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑌 ∈ 𝑃 )
48 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑋 ∈ 𝑃 )
49 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝐺 ∈ TarskiG )
50 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑤 ∈ 𝑃 )
51 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑣 ≠ 𝑤 )
52 51 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑤 ≠ 𝑣 )
53 23 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝑌 ≠ 𝑋 )
54 1 3 29 46 47 48 49 50 4 52 53 hlcgrex ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝑣 ) 𝑤 ∧ ( 𝑣 − 𝑡 ) = ( 𝑌 − 𝑋 ) ) )
55 45 54 r19.29a ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
56 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
57 55 56 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )
58 57 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )
59 58 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )
60 59 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )
61 1 fvexi ⊢ 𝑃 ∈ V
62 61 2 11 elcgrabasi ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
63 60 62 r19.29vva ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝐸 ) ∼ 𝐸 )