Metamath Proof Explorer

Theorem angmndaddov1

Description: Value of the addition operation in the angle addition monoid, in case the first angle is neither zero nor 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 ) ) ) ≠ ∅ ) ) ”⟩ ) )
angmndaddov1.x ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
angmndaddov1.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
angmndaddov1.1 ⊢ ( 𝜑 → ⟨“ 𝑍 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
angmndaddov1.2 ⊢ ( 𝜑 → ( 𝑌 − 𝑆 ) = ( 𝑉 − 𝑈 ) )
angmndaddov1.3 ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑆 𝐼 𝑋 ) ) ≠ ∅ )
Assertion angmndaddov1 ( 𝜑 → ( ⟨“ 𝑋 𝑌 𝑍 ”⟩ + ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) = ⟨“ 𝑋 𝑌 𝑆 ”⟩ )

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