Metamath Proof Explorer


Theorem addsdi

Description: Distributive law for surreal numbers. Commuted form of part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Assertion addsdi ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐴 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) )
2 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s 𝑦 ) = ( 𝑥𝑂 ·s 𝑦 ) )
3 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s 𝑧 ) = ( 𝑥𝑂 ·s 𝑧 ) )
4 2 3 oveq12d ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) )
5 1 4 eqeq12d ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) ↔ ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ) )
6 oveq1 ( 𝑦 = 𝑦𝑂 → ( 𝑦 +s 𝑧 ) = ( 𝑦𝑂 +s 𝑧 ) )
7 6 oveq2d ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) )
8 oveq2 ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝑂 ·s 𝑦𝑂 ) )
9 8 oveq1d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) )
10 7 9 eqeq12d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ↔ ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ) )
11 oveq2 ( 𝑧 = 𝑧𝑂 → ( 𝑦𝑂 +s 𝑧 ) = ( 𝑦𝑂 +s 𝑧𝑂 ) )
12 11 oveq2d ( 𝑧 = 𝑧𝑂 → ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
13 oveq2 ( 𝑧 = 𝑧𝑂 → ( 𝑥𝑂 ·s 𝑧 ) = ( 𝑥𝑂 ·s 𝑧𝑂 ) )
14 13 oveq2d ( 𝑧 = 𝑧𝑂 → ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
15 12 14 eqeq12d ( 𝑧 = 𝑧𝑂 → ( ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ↔ ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) )
16 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
17 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s 𝑦𝑂 ) = ( 𝑥𝑂 ·s 𝑦𝑂 ) )
18 oveq1 ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s 𝑧𝑂 ) = ( 𝑥𝑂 ·s 𝑧𝑂 ) )
19 17 18 oveq12d ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
20 16 19 eqeq12d ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ↔ ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) )
21 oveq1 ( 𝑦 = 𝑦𝑂 → ( 𝑦 +s 𝑧𝑂 ) = ( 𝑦𝑂 +s 𝑧𝑂 ) )
22 21 oveq2d ( 𝑦 = 𝑦𝑂 → ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
23 oveq2 ( 𝑦 = 𝑦𝑂 → ( 𝑥 ·s 𝑦 ) = ( 𝑥 ·s 𝑦𝑂 ) )
24 23 oveq1d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) )
25 22 24 eqeq12d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ↔ ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) )
26 21 oveq2d ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
27 8 oveq1d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
28 26 27 eqeq12d ( 𝑦 = 𝑦𝑂 → ( ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ↔ ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) )
29 11 oveq2d ( 𝑧 = 𝑧𝑂 → ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) )
30 oveq2 ( 𝑧 = 𝑧𝑂 → ( 𝑥 ·s 𝑧 ) = ( 𝑥 ·s 𝑧𝑂 ) )
31 30 oveq2d ( 𝑧 = 𝑧𝑂 → ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) )
32 29 31 eqeq12d ( 𝑧 = 𝑧𝑂 → ( ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ↔ ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) )
33 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( 𝐴 ·s ( 𝑦 +s 𝑧 ) ) )
34 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 ·s 𝑦 ) = ( 𝐴 ·s 𝑦 ) )
35 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 ·s 𝑧 ) = ( 𝐴 ·s 𝑧 ) )
36 34 35 oveq12d ( 𝑥 = 𝐴 → ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) = ( ( 𝐴 ·s 𝑦 ) +s ( 𝐴 ·s 𝑧 ) ) )
37 33 36 eqeq12d ( 𝑥 = 𝐴 → ( ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) ↔ ( 𝐴 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝐴 ·s 𝑦 ) +s ( 𝐴 ·s 𝑧 ) ) ) )
38 oveq1 ( 𝑦 = 𝐵 → ( 𝑦 +s 𝑧 ) = ( 𝐵 +s 𝑧 ) )
39 38 oveq2d ( 𝑦 = 𝐵 → ( 𝐴 ·s ( 𝑦 +s 𝑧 ) ) = ( 𝐴 ·s ( 𝐵 +s 𝑧 ) ) )
40 oveq2 ( 𝑦 = 𝐵 → ( 𝐴 ·s 𝑦 ) = ( 𝐴 ·s 𝐵 ) )
41 40 oveq1d ( 𝑦 = 𝐵 → ( ( 𝐴 ·s 𝑦 ) +s ( 𝐴 ·s 𝑧 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) )
42 39 41 eqeq12d ( 𝑦 = 𝐵 → ( ( 𝐴 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝐴 ·s 𝑦 ) +s ( 𝐴 ·s 𝑧 ) ) ↔ ( 𝐴 ·s ( 𝐵 +s 𝑧 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) ) )
43 oveq2 ( 𝑧 = 𝐶 → ( 𝐵 +s 𝑧 ) = ( 𝐵 +s 𝐶 ) )
44 43 oveq2d ( 𝑧 = 𝐶 → ( 𝐴 ·s ( 𝐵 +s 𝑧 ) ) = ( 𝐴 ·s ( 𝐵 +s 𝐶 ) ) )
45 oveq2 ( 𝑧 = 𝐶 → ( 𝐴 ·s 𝑧 ) = ( 𝐴 ·s 𝐶 ) )
46 45 oveq2d ( 𝑧 = 𝐶 → ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝐶 ) ) )
47 44 46 eqeq12d ( 𝑧 = 𝐶 → ( ( 𝐴 ·s ( 𝐵 +s 𝑧 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) ↔ ( 𝐴 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝐶 ) ) ) )
48 simpl1 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → 𝑥 No )
49 simpl2 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → 𝑦 No )
50 simpl3 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → 𝑧 No )
51 simpr21 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) )
52 simpr23 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) )
53 simpr12 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) )
54 elun1 ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
55 54 adantr ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
56 elun1 ( 𝑦𝐿 ∈ ( L ‘ 𝑦 ) → 𝑦𝐿 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
57 56 adantl ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → 𝑦𝐿 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
58 48 49 50 51 52 53 55 57 addsdilem3 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) ) → ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) )
59 58 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) ↔ 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
60 59 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
61 60 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } )
62 simpr3 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) )
63 simpr13 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
64 54 adantr ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
65 elun1 ( 𝑧𝐿 ∈ ( L ‘ 𝑧 ) → 𝑧𝐿 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
66 65 adantl ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → 𝑧𝐿 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
67 48 49 50 51 62 63 64 66 addsdilem4 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) ) → ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) )
68 67 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) ↔ 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) ) )
69 68 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) ) )
70 69 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } )
71 61 70 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ) )
72 elun2 ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
73 72 adantr ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
74 elun2 ( 𝑦𝑅 ∈ ( R ‘ 𝑦 ) → 𝑦𝑅 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
75 74 adantl ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → 𝑦𝑅 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
76 48 49 50 51 52 53 73 75 addsdilem3 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) ) → ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) )
77 76 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) ↔ 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
78 77 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
79 78 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } )
80 72 adantr ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
81 elun2 ( 𝑧𝑅 ∈ ( R ‘ 𝑧 ) → 𝑧𝑅 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
82 81 adantl ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → 𝑧𝑅 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
83 48 49 50 51 62 63 80 82 addsdilem4 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) )
84 83 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) ↔ 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) ) )
85 84 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) ) )
86 85 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } )
87 79 86 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) )
88 71 87 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) ) )
89 un4 ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) )
90 88 89 eqtrdi ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) ) )
91 54 adantr ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
92 74 adantl ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) → 𝑦𝑅 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
93 48 49 50 51 52 53 91 92 addsdilem3 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) ) → ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) )
94 93 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) ↔ 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
95 94 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
96 95 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } )
97 54 adantr ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
98 81 adantl ( ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) → 𝑧𝑅 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
99 48 49 50 51 62 63 97 98 addsdilem4 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) )
100 99 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∧ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) ↔ 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) ) )
101 100 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) ) )
102 101 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } )
103 96 102 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ) )
104 72 adantr ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
105 56 adantl ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) → 𝑦𝐿 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
106 48 49 50 51 52 53 104 105 addsdilem3 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) ) → ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) )
107 106 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) ↔ 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
108 107 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) ) )
109 108 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } )
110 72 adantr ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
111 65 adantl ( ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) → 𝑧𝐿 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
112 48 49 50 51 62 63 110 111 addsdilem4 ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) ) → ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) )
113 112 eqeq2d ( ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∧ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) ) ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) ↔ 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) ) )
114 113 2rexbidva ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) ) )
115 114 abbidv ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } )
116 109 115 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) = ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) )
117 103 116 uneq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) ) )
118 un4 ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) )
119 117 118 eqtrdi ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) ) )
120 90 119 oveq12d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ) |s ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ) ) = ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) ) |s ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) ) ) )
121 48 49 50 addsdilem1 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ) |s ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦 +s 𝑧𝑅 ) ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝑧 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧 ) ) +s ( 𝑥 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦 +s 𝑧𝐿 ) ) ) } ) ) ) )
122 48 49 50 addsdilem2 ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) = ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝐿 ·s 𝑧𝐿 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝑅 ·s 𝑧𝑅 ) ) ) } ) ) |s ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝐿 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑦𝑅 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( ( 𝑥𝑅 ·s 𝑦 ) +s ( 𝑥 ·s 𝑦𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑦𝐿 ) ) +s ( 𝑥 ·s 𝑧 ) ) } ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝐿 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝑅 ) ) -s ( 𝑥𝐿 ·s 𝑧𝑅 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝑧 ) 𝑎 = ( ( 𝑥 ·s 𝑦 ) +s ( ( ( 𝑥𝑅 ·s 𝑧 ) +s ( 𝑥 ·s 𝑧𝐿 ) ) -s ( 𝑥𝑅 ·s 𝑧𝐿 ) ) ) } ) ) ) )
123 120 121 122 3eqtr4d ( ( ( 𝑥 No 𝑦 No 𝑧 No ) ∧ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) ) → ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) )
124 123 ex ( ( 𝑥 No 𝑦 No 𝑧 No ) → ( ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥𝑂 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦𝑂 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥𝑂 ·s 𝑦 ) +s ( 𝑥𝑂 ·s 𝑧 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 ·s ( 𝑦𝑂 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦𝑂 ) +s ( 𝑥 ·s 𝑧 ) ) ) ∧ ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( 𝑥 ·s ( 𝑦 +s 𝑧𝑂 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧𝑂 ) ) ) → ( 𝑥 ·s ( 𝑦 +s 𝑧 ) ) = ( ( 𝑥 ·s 𝑦 ) +s ( 𝑥 ·s 𝑧 ) ) ) )
125 5 10 15 20 25 28 32 37 42 47 124 no3inds ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐴 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝐶 ) ) )