Metamath Proof Explorer

Theorem angmndaddov2

Description: Value of the addition operation in the angle addition monoid, in case the first angle is zero or flat. (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 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
angmndaddov.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
angmndaddov2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
angmndaddov2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
angmndaddov2.1 ⊢ ( 𝜑 → ⟨“ 𝑊 𝑉 𝑆 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
angmndaddov2.2 ⊢ ( 𝜑 → ( 𝑉 − 𝑆 ) = ( 𝑌 − 𝑋 ) )
Assertion angmndaddov2 ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ + ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) = ⟨“ 𝑈 𝑉 𝑆 ”⟩ )

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 angmndaddov.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
19 angmndaddov2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
20 angmndaddov2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
21 angmndaddov2.1 ⊢ ( 𝜑 → ⟨“ 𝑊 𝑉 𝑆 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
22 angmndaddov2.2 ⊢ ( 𝜑 → ( 𝑉 − 𝑆 ) = ( 𝑌 − 𝑋 ) )
23 18 a1i ⊢ ( 𝜑 → + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) )
24 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
26 25 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) )
27 s3fv0 ⊢ ( 𝑋 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑋 )
28 11 27 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑋 )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 0 ) = 𝑋 )
30 26 29 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 0 ) = 𝑋 )
31 25 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) )
32 s3fv1 ⊢ ( 𝑌 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑌 )
33 12 32 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑌 )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 1 ) = 𝑌 )
35 31 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 1 ) = 𝑌 )
36 25 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 2 ) = ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) )
37 s3fv2 ⊢ ( 𝑍 ∈ 𝑃 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑍 )
38 13 37 syl ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑍 )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ ‘ 2 ) = 𝑍 )
40 36 39 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 2 ) = 𝑍 )
41 35 40 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) = ( 𝑌 𝐿 𝑍 ) )
42 24 30 41 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) )
43 42 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) = ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
45 44 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 0 ) = ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 0 ) )
46 s3fv0 ⊢ ( 𝑈 ∈ 𝑃 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 0 ) = 𝑈 )
47 8 46 syl ⊢ ( 𝜑 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 0 ) = 𝑈 )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 0 ) = 𝑈 )
49 45 48 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 0 ) = 𝑈 )
50 44 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 1 ) = ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 1 ) )
51 s3fv1 ⊢ ( 𝑉 ∈ 𝑃 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 1 ) = 𝑉 )
52 9 51 syl ⊢ ( 𝜑 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 1 ) = 𝑉 )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 1 ) = 𝑉 )
54 50 53 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 1 ) = 𝑉 )
55 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑆 ∈ 𝑃 )
56 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝐺 ∈ TarskiG )
57 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑊 ∈ 𝑃 )
58 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑉 ∈ 𝑃 )
59 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑋 ∈ 𝑃 )
60 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑌 ∈ 𝑃 )
61 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑍 ∈ 𝑃 )
62 15 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑉 )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑊 ≠ 𝑉 )
64 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑉 ≠ 𝑊 )
65 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑋 ≠ 𝑌 )
66 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑌 ≠ 𝑍 )
67 1 2 3 4 5 6 56 57 58 57 59 60 61 63 64 65 66 24 angmndaddov2lem ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
68 44 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 2 ) = ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 2 ) )
69 s3fv2 ⊢ ( 𝑊 ∈ 𝑃 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 2 ) = 𝑊 )
70 10 69 syl ⊢ ( 𝜑 → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 2 ) = 𝑊 )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ 𝑈 𝑉 𝑊 ”⟩ ‘ 2 ) = 𝑊 )
72 68 71 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑓 ‘ 2 ) = 𝑊 )
73 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑠 = 𝑠 )
74 72 54 73 s3eqd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ = ⟨“ 𝑊 𝑉 𝑠 ”⟩ )
75 74 25 breq12d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ↔ ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) )
76 54 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( 𝑉 − 𝑠 ) )
77 35 30 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) = ( 𝑌 − 𝑋 ) )
78 76 77 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ↔ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) )
79 75 78 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ↔ ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ) )
80 79 bicomd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ↔ ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) )
81 80 reubidv ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑊 𝑉 𝑠 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ( 𝑉 − 𝑠 ) = ( 𝑌 − 𝑋 ) ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) )
82 67 81 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) )
83 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ⟨“ 𝑊 𝑉 𝑆 ”⟩ ∼ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
84 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → 𝑆 = 𝑆 )
85 72 54 84 s3eqd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ = ⟨“ 𝑊 𝑉 𝑆 ”⟩ )
86 83 85 25 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ ∼ 𝑒 )
87 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( 𝑉 − 𝑆 ) = ( 𝑌 − 𝑋 ) )
88 54 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( 𝑉 − 𝑆 ) )
89 87 88 77 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) )
90 eqidd ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ 2 ) = ( 𝑓 ‘ 2 ) )
91 eqidd ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 1 ) )
92 id ⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
93 90 91 92 s3eqd ⊢ ( 𝑠 = 𝑆 → ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ = ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ )
94 93 breq1d ⊢ ( 𝑠 = 𝑆 → ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ↔ ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ ∼ 𝑒 ) )
95 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − 𝑆 ) )
96 95 eqeq1d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) )
97 94 96 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ↔ ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) )
98 97 riota2 ⊢ ( ( 𝑆 ∈ 𝑃 ∧ ∃! 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) → ( ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ↔ ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) = 𝑆 ) )
99 98 biimpa ⊢ ( ( ( 𝑆 ∈ 𝑃 ∧ ∃! 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ∧ ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑆 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑆 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) → ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) = 𝑆 )
100 55 82 86 89 99 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) = 𝑆 )
101 49 54 100 s3eqd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ = ⟨“ 𝑈 𝑉 𝑆 ”⟩ )
102 43 101 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) → if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) = ⟨“ 𝑈 𝑉 𝑆 ”⟩ )
103 102 anasss ⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ 𝑓 = ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ) → if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) = ⟨“ 𝑈 𝑉 𝑆 ”⟩ )
104 1 fvexi ⊢ 𝑃 ∈ V
105 104 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
106 2 105 11 12 13 16 17 elcgrabasrd ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ 𝐴 )
107 2 105 8 9 10 14 15 elcgrabasrd ⊢ ( 𝜑 → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∈ 𝐴 )
108 22 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) = ( 𝑉 − 𝑆 ) )
109 16 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
110 1 4 3 7 12 11 9 20 108 109 tgcgrneq ⊢ ( 𝜑 → 𝑉 ≠ 𝑆 )
111 2 105 8 9 20 14 110 elcgrabasrd ⊢ ( 𝜑 → ⟨“ 𝑈 𝑉 𝑆 ”⟩ ∈ 𝐴 )
112 23 103 106 107 111 ovmpod ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ + ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) = ⟨“ 𝑈 𝑉 𝑆 ”⟩ )