Metamath Proof Explorer

Theorem angmgmaddcl

Description: Closure of 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 ) ) ) ≠ ∅ ) ) ”⟩ ) )
angmgmaddcl.1 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
angmgmaddcl.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
Assertion angmgmaddcl ( 𝜑 → ( 𝐸 + 𝐹 ) ∈ 𝐴 )

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 angmgmaddcl.1 ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
10 angmgmaddcl.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
11 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
12 11 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) → 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
13 12 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
14 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
15 13 14 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( 𝐸 + 𝐹 ) = ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) )
16 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
17 16 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
18 17 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝐺 ∈ TarskiG )
19 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑢 ∈ 𝑃 )
20 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑣 ∈ 𝑃 )
21 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑤 ∈ 𝑃 )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑥 ∈ 𝑃 )
23 22 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑥 ∈ 𝑃 )
24 23 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑥 ∈ 𝑃 )
25 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ 𝑃 )
26 25 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑦 ∈ 𝑃 )
27 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ 𝑃 )
28 27 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ 𝑃 )
29 28 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑧 ∈ 𝑃 )
30 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑢 ≠ 𝑣 )
31 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑣 ≠ 𝑤 )
32 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑥 ≠ 𝑦 )
33 simp-10r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑦 ≠ 𝑧 )
34 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) )
35 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑡 ∈ 𝑃 )
36 simprl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
37 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) )
38 1 2 3 4 5 6 18 19 20 21 24 26 29 30 31 32 33 8 34 35 36 37 angmgmaddov2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
39 15 38 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( 𝐸 + 𝐹 ) = ⟨“ 𝑢 𝑣 𝑡 ”⟩ )
40 1 fvexi ⊢ 𝑃 ∈ V
41 40 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑃 ∈ V )
42 37 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( 𝑦 − 𝑥 ) = ( 𝑣 − 𝑡 ) )
43 32 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑦 ≠ 𝑥 )
44 1 4 3 18 26 24 20 35 42 43 tgcgrneq ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → 𝑣 ≠ 𝑡 )
45 2 41 19 20 35 30 44 elcgrabasrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ⟨“ 𝑢 𝑣 𝑡 ”⟩ ∈ 𝐴 )
46 39 45 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
47 16 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝐺 ∈ TarskiG )
48 47 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝐺 ∈ TarskiG )
49 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑢 ∈ 𝑃 )
50 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑣 ∈ 𝑃 )
51 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑤 ∈ 𝑃 )
52 22 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) → 𝑥 ∈ 𝑃 )
53 52 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑥 ∈ 𝑃 )
54 25 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑦 ∈ 𝑃 )
55 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑧 ∈ 𝑃 )
56 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑢 ≠ 𝑣 )
57 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑣 ≠ 𝑤 )
58 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑥 ≠ 𝑦 )
59 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑦 ≠ 𝑧 )
60 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) )
61 1 2 3 4 5 6 48 49 50 51 53 54 55 56 57 58 59 60 angmgmaddov2lem ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) )
62 reurex ⊢ ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) → ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) )
63 61 62 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) )
64 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑤 = 𝑤 )
65 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑣 = 𝑣 )
66 id ⊢ ( 𝑠 = 𝑡 → 𝑠 = 𝑡 )
67 64 65 66 s3eqd ⊢ ( 𝑠 = 𝑡 → ⟨“ 𝑤 𝑣 𝑠 ”⟩ = ⟨“ 𝑤 𝑣 𝑡 ”⟩ )
68 67 breq1d ⊢ ( 𝑠 = 𝑡 → ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ↔ ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) )
69 oveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝑣 − 𝑠 ) = ( 𝑣 − 𝑡 ) )
70 69 eqeq1d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ↔ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) )
71 68 70 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) ↔ ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) ) )
72 71 cbvrexvw ⊢ ( ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑠 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑠 ) = ( 𝑦 − 𝑥 ) ) ↔ ∃ 𝑡 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) )
73 63 72 sylib ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃ 𝑡 ∈ 𝑃 ( ⟨“ 𝑤 𝑣 𝑡 ”⟩ ∼ ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑣 − 𝑡 ) = ( 𝑦 − 𝑥 ) ) )
74 46 73 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
75 11 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ )
76 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
77 75 76 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( 𝐸 + 𝐹 ) = ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) )
78 17 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝐺 ∈ TarskiG )
79 78 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝐺 ∈ TarskiG )
80 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑢 ∈ 𝑃 )
81 80 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑢 ∈ 𝑃 )
82 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑣 ∈ 𝑃 )
83 82 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑣 ∈ 𝑃 )
84 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑤 ∈ 𝑃 )
85 84 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑤 ∈ 𝑃 )
86 23 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑥 ∈ 𝑃 )
87 86 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑥 ∈ 𝑃 )
88 25 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑦 ∈ 𝑃 )
89 88 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑦 ∈ 𝑃 )
90 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑧 ∈ 𝑃 )
91 90 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑧 ∈ 𝑃 )
92 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑢 ≠ 𝑣 )
93 92 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑢 ≠ 𝑣 )
94 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑣 ≠ 𝑤 )
95 94 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑣 ≠ 𝑤 )
96 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑥 ≠ 𝑦 )
97 96 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑥 ≠ 𝑦 )
98 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → 𝑦 ≠ 𝑧 )
99 98 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑦 ≠ 𝑧 )
100 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) )
101 100 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) )
102 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑡 ∈ 𝑃 )
103 simpr1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ )
104 simpr2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) )
105 simpr3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ )
106 1 2 3 4 5 6 79 81 83 85 87 89 91 93 95 97 99 8 101 102 103 104 105 angmgmaddov1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( ⟨“ 𝑥 𝑦 𝑧 ”⟩ + ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) = ⟨“ 𝑥 𝑦 𝑡 ”⟩ )
107 77 106 eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( 𝐸 + 𝐹 ) = ⟨“ 𝑥 𝑦 𝑡 ”⟩ )
108 40 a1i ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑃 ∈ V )
109 104 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( 𝑣 − 𝑢 ) = ( 𝑦 − 𝑡 ) )
110 93 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑣 ≠ 𝑢 )
111 1 4 3 79 83 81 89 102 109 110 tgcgrneq ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → 𝑦 ≠ 𝑡 )
112 2 108 87 89 102 97 111 elcgrabasrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ⟨“ 𝑥 𝑦 𝑡 ”⟩ ∈ 𝐴 )
113 107 112 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
114 1 2 3 4 5 6 78 80 82 84 86 88 90 92 94 96 98 100 angmgmaddov1lem ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) )
115 reurex ⊢ ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) )
116 114 115 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) )
117 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑧 = 𝑧 )
118 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑦 = 𝑦 )
119 117 118 66 s3eqd ⊢ ( 𝑠 = 𝑡 → ⟨“ 𝑧 𝑦 𝑠 ”⟩ = ⟨“ 𝑧 𝑦 𝑡 ”⟩ )
120 119 breq1d ⊢ ( 𝑠 = 𝑡 → ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ↔ ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) )
121 oveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝑦 − 𝑠 ) = ( 𝑦 − 𝑡 ) )
122 121 eqeq1d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ↔ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ) )
123 oveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 𝐼 𝑥 ) = ( 𝑡 𝐼 𝑥 ) )
124 123 ineq2d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) = ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) )
125 124 neeq1d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ↔ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) )
126 120 122 125 3anbi123d ⊢ ( 𝑠 = 𝑡 → ( ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) ↔ ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) ) )
127 126 cbvrexvw ⊢ ( ∃ 𝑠 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑠 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑠 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑠 𝐼 𝑥 ) ) ≠ ∅ ) ↔ ∃ 𝑡 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) )
128 116 127 sylib ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ∃ 𝑡 ∈ 𝑃 ( ⟨“ 𝑧 𝑦 𝑡 ”⟩ ∼ ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑦 − 𝑡 ) = ( 𝑣 − 𝑢 ) ∧ ( ( 𝑦 𝐿 𝑧 ) ∩ ( 𝑡 𝐼 𝑥 ) ) ≠ ∅ ) )
129 113 128 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) ∧ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
130 exmidd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ∨ ¬ 𝑥 ∈ ( 𝑦 𝐿 𝑧 ) ) )
131 74 129 130 mpjaodan ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ 𝑢 ≠ 𝑣 ) ∧ 𝑣 ≠ 𝑤 ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
132 131 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ) ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
133 132 anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
134 133 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ∃ 𝑤 ∈ 𝑃 ( 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
135 40 2 10 elcgrabasi ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
136 135 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝐹 = ⟨“ 𝑢 𝑣 𝑤 ”⟩ ∧ ( 𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤 ) ) )
137 134 136 r19.29vva ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
138 137 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
139 138 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
140 139 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) ) → ( 𝐸 + 𝐹 ) ∈ 𝐴 )
141 40 2 9 elcgrabasi ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝐸 = ⟨“ 𝑥 𝑦 𝑧 ”⟩ ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ) ) )
142 140 141 r19.29vva ⊢ ( 𝜑 → ( 𝐸 + 𝐹 ) ∈ 𝐴 )