Metamath Proof Explorer

Theorem addsdilem1

Description: Lemma for surreal distribution. Expand the left hand side of the main expression. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses addsdilem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsdilem.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
addsdilem.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion addsdilem1 ( 𝜑 → ( 𝐴 ·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 𝑧𝐿 ) ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 addsdilem.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 addsdilem.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 lltropt ⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
5 4 a1i ⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
6 2 3 addscut2 ⊢ ( 𝜑 → ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) <<s ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) )
7 lrcut ⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
8 1 7 syl ⊢ ( 𝜑 → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
9 8 eqcomd ⊢ ( 𝜑 → 𝐴 = ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) )
10 addsval2 ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐵 +s 𝐶 ) = ( ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) |s ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) ) )
11 2 3 10 syl2anc ⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) = ( ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) |s ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) ) )
12 5 6 9 11 mulsunif ⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 +s 𝐶 ) ) = ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } ) |s ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } ) ) )
13 unab ⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( 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 ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) }
14 r19.43 ⊢ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( 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 ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
15 rexun ⊢ ( ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
16 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝑦𝐿 +s 𝐶 ) ↔ 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ) )
17 16 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ) )
18 17 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
19 rexcom4 ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
20 ovex ⊢ ( 𝑦𝐿 +s 𝐶 ) ∈ V
21 oveq2 ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) )
22 21 oveq2d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
23 oveq2 ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( 𝑥𝐿 ·s 𝑏 ) = ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) )
24 22 23 oveq12d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
25 24 eqeq2d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ) )
26 20 25 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
27 26 rexbii ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
28 r19.41v ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
29 28 exbii ⊢ ( ∃ 𝑏 ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
30 19 27 29 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
31 18 30 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
32 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝐵 +s 𝑧𝐿 ) ↔ 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ) )
33 32 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ) )
34 33 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
35 rexcom4 ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
36 ovex ⊢ ( 𝐵 +s 𝑧𝐿 ) ∈ V
37 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) )
38 37 oveq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
39 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( 𝑥𝐿 ·s 𝑏 ) = ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) )
40 38 39 oveq12d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
41 40 eqeq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
42 36 41 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
43 42 rexbii ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
44 r19.41v ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
45 44 exbii ⊢ ( ∃ 𝑏 ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
46 35 43 45 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
47 34 46 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
48 31 47 orbi12i ⊢ ( ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
49 15 48 bitr2i ⊢ ( ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
50 49 rexbii ⊢ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
51 14 50 bitr3i ⊢ ( ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
52 51 abbii ⊢ { 𝑎 ∣ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) }
53 13 52 eqtri ⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) } ) = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) }
54 unab ⊢ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) }
55 r19.43 ⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( 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 ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
56 rexun ⊢ ( ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
57 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝑦𝑅 +s 𝐶 ) ↔ 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ) )
58 57 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ) )
59 58 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
60 rexcom4 ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
61 ovex ⊢ ( 𝑦𝑅 +s 𝐶 ) ∈ V
62 oveq2 ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) )
63 62 oveq2d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
64 oveq2 ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( 𝑥𝑅 ·s 𝑏 ) = ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) )
65 63 64 oveq12d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
66 65 eqeq2d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ) )
67 61 66 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
68 67 rexbii ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
69 r19.41v ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
70 69 exbii ⊢ ( ∃ 𝑏 ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
71 60 68 70 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
72 59 71 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
73 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝐵 +s 𝑧𝑅 ) ↔ 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ) )
74 73 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ) )
75 74 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
76 rexcom4 ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
77 ovex ⊢ ( 𝐵 +s 𝑧𝑅 ) ∈ V
78 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) )
79 78 oveq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
80 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( 𝑥𝑅 ·s 𝑏 ) = ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) )
81 79 80 oveq12d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
82 81 eqeq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
83 77 82 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
84 83 rexbii ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
85 r19.41v ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
86 85 exbii ⊢ ( ∃ 𝑏 ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
87 76 84 86 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
88 75 87 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
89 72 88 orbi12i ⊢ ( ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
90 56 89 bitr2i ⊢ ( ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
91 90 rexbii ⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
92 55 91 bitr3i ⊢ ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
93 92 abbii ⊢ { 𝑎 ∣ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) }
94 54 93 eqtri ⊢ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) } ) = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) }
95 53 94 uneq12i ⊢ ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( 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 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } )
96 unab ⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( 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 ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) }
97 r19.43 ⊢ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( 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 ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
98 rexun ⊢ ( ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
99 58 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
100 rexcom4 ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
101 62 oveq2d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
102 oveq2 ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( 𝑥𝐿 ·s 𝑏 ) = ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) )
103 101 102 oveq12d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
104 103 eqeq2d ⊢ ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ) )
105 61 104 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
106 105 rexbii ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
107 r19.41v ⊢ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
108 107 exbii ⊢ ( ∃ 𝑏 ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
109 100 106 108 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑏 = ( 𝑦𝑅 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
110 99 109 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) )
111 74 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
112 rexcom4 ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
113 78 oveq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
114 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( 𝑥𝐿 ·s 𝑏 ) = ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) )
115 113 114 oveq12d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
116 115 eqeq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) → ( 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
117 77 116 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
118 117 rexbii ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
119 r19.41v ⊢ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
120 119 exbii ⊢ ( ∃ 𝑏 ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) )
121 112 118 120 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝑅 ) ∧ 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
122 111 121 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) )
123 110 122 orbi12i ⊢ ( ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) )
124 98 123 bitr2i ⊢ ( ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
125 124 rexbii ⊢ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
126 97 125 bitr3i ⊢ ( ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) )
127 126 abbii ⊢ { 𝑎 ∣ ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) }
128 96 127 eqtri ⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) -s ( 𝑥𝐿 ·s ( 𝑦𝑅 +s 𝐶 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) -s ( 𝑥𝐿 ·s ( 𝐵 +s 𝑧𝑅 ) ) ) } ) = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) }
129 unab ⊢ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) }
130 r19.43 ⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( 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 ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
131 rexun ⊢ ( ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
132 17 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
133 rexcom4 ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
134 21 oveq2d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
135 oveq2 ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( 𝑥𝑅 ·s 𝑏 ) = ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) )
136 134 135 oveq12d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
137 136 eqeq2d ⊢ ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ) )
138 20 137 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
139 138 rexbii ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ∃ 𝑏 ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
140 r19.41v ⊢ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
141 140 exbii ⊢ ( ∃ 𝑏 ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ( 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
142 133 139 141 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝑦𝐿 +s 𝐶 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
143 132 142 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) )
144 33 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
145 rexcom4 ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
146 37 oveq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) = ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
147 oveq2 ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( 𝑥𝑅 ·s 𝑏 ) = ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) )
148 146 147 oveq12d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
149 148 eqeq2d ⊢ ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) → ( 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
150 36 149 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
151 150 rexbii ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ∃ 𝑏 ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
152 r19.41v ⊢ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
153 152 exbii ⊢ ( ∃ 𝑏 ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) ( 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) )
154 145 151 153 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑏 = ( 𝐵 +s 𝑧𝐿 ) ∧ 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
155 144 154 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ↔ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) )
156 143 155 orbi12i ⊢ ( ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ∨ ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) ) ↔ ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) )
157 131 156 bitr2i ⊢ ( ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
158 157 rexbii ⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
159 130 158 bitr3i ⊢ ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) )
160 159 abbii ⊢ { 𝑎 ∣ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) }
161 129 160 eqtri ⊢ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) -s ( 𝑥𝑅 ·s ( 𝑦𝐿 +s 𝐶 ) ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) -s ( 𝑥𝑅 ·s ( 𝐵 +s 𝑧𝐿 ) ) ) } ) = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) }
162 128 161 uneq12i ⊢ ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( 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 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } )
163 95 162 oveq12i ⊢ ( ( ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( 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 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } ) |s ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝑅 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝑦𝑅 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝑅 ) } ) 𝑎 = ( ( ( 𝑥𝐿 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝐿 ·s 𝑏 ) ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑡 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑡 = ( 𝑦𝐿 +s 𝐶 ) } ∪ { 𝑡 ∣ ∃ 𝑧𝐿 ∈ ( L ‘ 𝐶 ) 𝑡 = ( 𝐵 +s 𝑧𝐿 ) } ) 𝑎 = ( ( ( 𝑥𝑅 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s 𝑏 ) ) -s ( 𝑥𝑅 ·s 𝑏 ) ) } ) )
164 12 163 eqtr4di ⊢ ( 𝜑 → ( 𝐴 ·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 𝑧𝐿 ) ) ) } ) ) ) )