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 𝑧𝐿 ) ) ) } ) ) ) )