Metamath Proof Explorer

Theorem angmndaddeu6

Description: There exists a unique point s satisfying the conditions of angle addition. Case where the first angle is a zero angle, and the second angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmndadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmndadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmndadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
angmndadd.d ⊢ − = ( dist ‘ 𝐺 )
angmndadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmndadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
angmndadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
angmndaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
angmndaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
angmndaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
angmndaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
angmndaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
angmndaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
angmndaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
angmndaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
angmndaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
angmndaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
angmndaddeu6.1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
angmndaddeu6.2 ⊢ ( 𝜑 → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
Assertion angmndaddeu6 ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 angmndadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmndadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmndadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmndadd.d ⊢ − = ( dist ‘ 𝐺 )
5 angmndadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmndadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmndadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 angmndaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 angmndaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 angmndaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 angmndaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 angmndaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 angmndaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 angmndaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
15 angmndaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
16 angmndaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
17 angmndaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
18 angmndaddeu6.1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
19 angmndaddeu6.2 ⊢ ( 𝜑 → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
20 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
21 17 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
22 14 necomd ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
23 1 3 20 12 9 8 7 13 4 21 22 hlcgreu ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
24 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝐺 ∈ TarskiG )
25 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ 𝑃 )
26 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ∈ 𝑃 )
27 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ 𝑃 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
29 1 3 20 25 26 27 24 28 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑠 )
30 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
31 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ∈ 𝑃 )
32 1 5 20 24 29 30 27 31 zerocgra ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
33 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
34 32 33 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
35 34 anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
36 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ∈ 𝑃 )
37 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ∈ 𝑃 )
38 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑌 ∈ 𝑃 )
39 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝐺 ∈ TarskiG )
40 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ∈ 𝑃 )
41 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑉 ∈ 𝑃 )
42 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑊 ∈ 𝑃 )
43 5 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ∼ = ( cgrA ‘ 𝐺 ) )
44 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
45 43 44 breqdi ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
46 1 3 39 20 36 38 37 40 41 42 45 cgracom ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
47 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
48 1 3 4 39 40 41 42 36 38 37 46 20 47 cgrahl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑍 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑠 )
49 1 3 20 36 37 38 39 48 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 )
50 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
51 49 50 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) → ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
52 51 anasss ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) → ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )
53 35 52 impbida ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑃 ) → ( ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) )
54 53 reubidva ⊢ ( 𝜑 → ( ∃! 𝑠 ∈ 𝑃 ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑍 ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ) )
55 23 54 mpbid ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) )