Step | Hyp | Ref
| Expression |
1 | | lltropt 27296 |
. . . 4
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴)) |
3 | | addsdilem.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ No
) |
4 | | addsdilem.3 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ No
) |
5 | 3, 4 | addscut2 27392 |
. . 3
⊢ (𝜑 → ({𝑡 ∣ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}) <<s ({𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)})) |
6 | | addsdilem.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ No
) |
7 | | lrcut 27326 |
. . . . 5
⊢ (𝐴 ∈
No → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) |
9 | 8 | eqcomd 2738 |
. . 3
⊢ (𝜑 → 𝐴 = (( L ‘𝐴) |s ( R ‘𝐴))) |
10 | | addsval2 27376 |
. . . 4
⊢ ((𝐵 ∈
No ∧ 𝐶 ∈
No ) → (𝐵 +s 𝐶) = (({𝑡 ∣ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}) |s ({𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}))) |
11 | 3, 4, 10 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐵 +s 𝐶) = (({𝑡 ∣ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}) |s ({𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)} ∪ {𝑡 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}))) |
12 | 2, 5, 9, 11 | mulsunif 27534 |
. 2
⊢ (𝜑 → (𝐴 ·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 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 3122 |
. . . . . . 7
⊢
(∃𝑥𝐿 ∈ ( 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 4187 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
({𝑡 ∣ ∃𝑦𝐿 ∈ ( 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 2736 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 = (𝑦𝐿 +s 𝐶) ↔ 𝑏 = (𝑦𝐿 +s 𝐶))) |
17 | 16 | rexbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶) ↔ ∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶))) |
18 | 17 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
19 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
20 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝐿
+s 𝐶) ∈
V |
21 | | oveq2 7402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (𝐴 ·s 𝑏) = (𝐴 ·s (𝑦𝐿 +s 𝐶))) |
22 | 21 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → ((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) = ((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))) |
23 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (𝑥𝐿 ·s
𝑏) = (𝑥𝐿 ·s
(𝑦𝐿
+s 𝐶))) |
24 | 22, 23 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)) =
(((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝐿 +s 𝐶)))) |
25 | 24 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝐿 +s 𝐶))))) |
26 | 20, 25 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝐿 +s 𝐶)))) |
27 | 26 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝐶)))) |
28 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ (∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
29 | 28 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
30 | 19, 27, 29 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝐶)))) |
31 | 18, 30 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝐿
+s 𝐶)))) |
32 | | eqeq1 2736 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 = (𝐵 +s 𝑧𝐿) ↔ 𝑏 = (𝐵 +s 𝑧𝐿))) |
33 | 32 | rexbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L
‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿))) |
34 | 33 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝐿 ∈ ( L
‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
35 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏∃𝑧𝐿 ∈ ( L
‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
36 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (𝐵 +s 𝑧𝐿) ∈
V |
37 | | oveq2 7402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (𝐴 ·s 𝑏) = (𝐴 ·s (𝐵 +s 𝑧𝐿))) |
38 | 37 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → ((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏)) =
((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿)))) |
39 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (𝑥𝐿
·s 𝑏) =
(𝑥𝐿
·s (𝐵
+s 𝑧𝐿))) |
40 | 38, 39 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏))
-s (𝑥𝐿 ·s
𝑏)) = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝐿)))) |
41 | 40 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿))) -s (𝑥𝐿
·s (𝐵
+s 𝑧𝐿))))) |
42 | 36, 41 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿))) -s (𝑥𝐿
·s (𝐵
+s 𝑧𝐿)))) |
43 | 42 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝐿)))) |
44 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
45 | 44 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑧𝐿 ∈ ( L ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
46 | 35, 43, 45 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝐿)))) |
47 | 34, 46 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝐿 ∈ ( L
‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝐿)))) |
48 | 31, 47 | orbi12i 913 |
. . . . . . . . 9
⊢
((∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( 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 275 |
. . . . . . . 8
⊢
((∃𝑦𝐿 ∈ ( 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 3094 |
. . . . . . 7
⊢
(∃𝑥𝐿 ∈ ( 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 276 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( 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 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( 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 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 3122 |
. . . . . . 7
⊢
(∃𝑥𝑅 ∈ ( 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 4187 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
({𝑡 ∣ ∃𝑦𝑅 ∈ ( 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 2736 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 = (𝑦𝑅 +s 𝐶) ↔ 𝑏 = (𝑦𝑅 +s 𝐶))) |
58 | 57 | rexbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶) ↔ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶))) |
59 | 58 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
60 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
61 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝑅
+s 𝐶) ∈
V |
62 | | oveq2 7402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (𝐴 ·s 𝑏) = (𝐴 ·s (𝑦𝑅 +s 𝐶))) |
63 | 62 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → ((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) = ((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))) |
64 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (𝑥𝑅 ·s
𝑏) = (𝑥𝑅 ·s
(𝑦𝑅
+s 𝐶))) |
65 | 63, 64 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)) =
(((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝑅 +s 𝐶)))) |
66 | 65 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝑅 +s 𝐶))))) |
67 | 61, 66 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝑅 +s 𝐶)))) |
68 | 67 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝐶)))) |
69 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ (∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
70 | 69 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
71 | 60, 68, 70 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝐶)))) |
72 | 59, 71 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝑅
+s 𝐶)))) |
73 | | eqeq1 2736 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 = (𝐵 +s 𝑧𝑅) ↔ 𝑏 = (𝐵 +s 𝑧𝑅))) |
74 | 73 | rexbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R
‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅))) |
75 | 74 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
76 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏∃𝑧𝑅 ∈ ( R
‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
77 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (𝐵 +s 𝑧𝑅) ∈
V |
78 | | oveq2 7402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (𝐴 ·s 𝑏) = (𝐴 ·s (𝐵 +s 𝑧𝑅))) |
79 | 78 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → ((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏)) =
((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅)))) |
80 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (𝑥𝑅
·s 𝑏) =
(𝑥𝑅
·s (𝐵
+s 𝑧𝑅))) |
81 | 79, 80 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏))
-s (𝑥𝑅 ·s
𝑏)) = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝑅)))) |
82 | 81 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅))) -s (𝑥𝑅
·s (𝐵
+s 𝑧𝑅))))) |
83 | 77, 82 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅))) -s (𝑥𝑅
·s (𝐵
+s 𝑧𝑅)))) |
84 | 83 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝑅)))) |
85 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
86 | 85 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑧𝑅 ∈ ( R ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
87 | 76, 84, 86 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝑅)))) |
88 | 75, 87 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝑅)))) |
89 | 72, 88 | orbi12i 913 |
. . . . . . . . 9
⊢
((∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( 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 275 |
. . . . . . . 8
⊢
((∃𝑦𝑅 ∈ ( 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 3094 |
. . . . . . 7
⊢
(∃𝑥𝑅 ∈ ( 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 276 |
. . . . . 6
⊢
((∃𝑥𝑅 ∈ ( 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 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝑅 ∈ ( 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 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 4158 |
. . 3
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 3122 |
. . . . . . 7
⊢
(∃𝑥𝐿 ∈ ( 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 4187 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
({𝑡 ∣ ∃𝑦𝑅 ∈ ( 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 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
100 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
101 | 62 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → ((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) = ((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))) |
102 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (𝑥𝐿 ·s
𝑏) = (𝑥𝐿 ·s
(𝑦𝑅
+s 𝐶))) |
103 | 101, 102 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)) =
(((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝑅 +s 𝐶)))) |
104 | 103 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑦𝑅 +s 𝐶) → (𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝑅 +s 𝐶))))) |
105 | 61, 104 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝑅 +s 𝐶))) -s (𝑥𝐿
·s (𝑦𝑅 +s 𝐶)))) |
106 | 105 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑏(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝐶)))) |
107 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ (∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
108 | 107 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
109 | 100, 106,
108 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (𝑦𝑅 +s 𝐶) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝐶)))) |
110 | 99, 109 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (𝑦𝑅 +s 𝐶)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑦𝑅 ∈ ( R ‘𝐵)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝑅
+s 𝐶)))
-s (𝑥𝐿 ·s
(𝑦𝑅
+s 𝐶)))) |
111 | 74 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
112 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏∃𝑧𝑅 ∈ ( R
‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
113 | 78 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → ((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏)) =
((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅)))) |
114 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (𝑥𝐿
·s 𝑏) =
(𝑥𝐿
·s (𝐵
+s 𝑧𝑅))) |
115 | 113, 114 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏))
-s (𝑥𝐿 ·s
𝑏)) = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝑅)))) |
116 | 115 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝐵 +s 𝑧𝑅) → (𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅))) -s (𝑥𝐿
·s (𝐵
+s 𝑧𝑅))))) |
117 | 77, 116 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ 𝑎 = (((𝑥𝐿
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝑅))) -s (𝑥𝐿
·s (𝐵
+s 𝑧𝑅)))) |
118 | 117 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝑅)))) |
119 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑧𝑅 ∈ ( R ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
120 | 119 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑧𝑅 ∈ ( R ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))) |
121 | 112, 118,
120 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑧𝑅 ∈ ( R ‘𝐶)𝑏 = (𝐵 +s 𝑧𝑅) ∧ 𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏)))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝑅)))) |
122 | 111, 121 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐶)𝑡 = (𝐵 +s 𝑧𝑅)}𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝐿
·s 𝑏))
↔ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑥𝐿 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝑅)))
-s (𝑥𝐿 ·s
(𝐵 +s 𝑧𝑅)))) |
123 | 110, 122 | orbi12i 913 |
. . . . . . . . 9
⊢
((∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝑅 ∈ ( 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 275 |
. . . . . . . 8
⊢
((∃𝑦𝑅 ∈ ( 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 3094 |
. . . . . . 7
⊢
(∃𝑥𝐿 ∈ ( 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 276 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( 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 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( 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 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 3122 |
. . . . . . 7
⊢
(∃𝑥𝑅 ∈ ( 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 4187 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
({𝑡 ∣ ∃𝑦𝐿 ∈ ( 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 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
133 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
134 | 21 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → ((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) = ((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))) |
135 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (𝑥𝑅 ·s
𝑏) = (𝑥𝑅 ·s
(𝑦𝐿
+s 𝐶))) |
136 | 134, 135 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)) =
(((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝐿 +s 𝐶)))) |
137 | 136 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑦𝐿 +s 𝐶) → (𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝐿 +s 𝐶))))) |
138 | 20, 137 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝑦𝐿 +s 𝐶))) -s (𝑥𝑅
·s (𝑦𝐿 +s 𝐶)))) |
139 | 138 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑏(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝐶)))) |
140 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ (∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
141 | 140 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
142 | 133, 139,
141 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (𝑦𝐿 +s 𝐶) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝐶)))) |
143 | 132, 142 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (𝑦𝐿 +s 𝐶)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑦𝐿 ∈ ( L ‘𝐵)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝑦𝐿
+s 𝐶)))
-s (𝑥𝑅 ·s
(𝑦𝐿
+s 𝐶)))) |
144 | 33 | rexab 3687 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝐿 ∈ ( L
‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
145 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏∃𝑧𝐿 ∈ ( L
‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
146 | 37 | oveq2d 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → ((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏)) =
((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿)))) |
147 | | oveq2 7402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (𝑥𝑅
·s 𝑏) =
(𝑥𝑅
·s (𝐵
+s 𝑧𝐿))) |
148 | 146, 147 | oveq12d 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s 𝑏))
-s (𝑥𝑅 ·s
𝑏)) = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝐿)))) |
149 | 148 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝐵 +s 𝑧𝐿) → (𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿))) -s (𝑥𝑅
·s (𝐵
+s 𝑧𝐿))))) |
150 | 36, 149 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ 𝑎 = (((𝑥𝑅
·s (𝐵
+s 𝐶))
+s (𝐴
·s (𝐵
+s 𝑧𝐿))) -s (𝑥𝑅
·s (𝐵
+s 𝑧𝐿)))) |
151 | 150 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)∃𝑏(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝐿)))) |
152 | | r19.41v 3188 |
. . . . . . . . . . . . 13
⊢
(∃𝑧𝐿 ∈ ( L ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
153 | 152 | exbii 1850 |
. . . . . . . . . . . 12
⊢
(∃𝑏∃𝑧𝐿 ∈ ( L ‘𝐶)(𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))) |
154 | 145, 151,
153 | 3bitr3ri 301 |
. . . . . . . . . . 11
⊢
(∃𝑏(∃𝑧𝐿 ∈ ( L ‘𝐶)𝑏 = (𝐵 +s 𝑧𝐿) ∧ 𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏)))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝐿)))) |
155 | 144, 154 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
{𝑡 ∣ ∃𝑧𝐿 ∈ ( L
‘𝐶)𝑡 = (𝐵 +s 𝑧𝐿)}𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s 𝑏)) -s (𝑥𝑅
·s 𝑏))
↔ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑥𝑅 ·s
(𝐵 +s 𝐶)) +s (𝐴 ·s (𝐵 +s 𝑧𝐿)))
-s (𝑥𝑅 ·s
(𝐵 +s 𝑧𝐿)))) |
156 | 143, 155 | orbi12i 913 |
. . . . . . . . 9
⊢
((∃𝑏 ∈
{𝑡 ∣ ∃𝑦𝐿 ∈ ( 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 275 |
. . . . . . . 8
⊢
((∃𝑦𝐿 ∈ ( 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 3094 |
. . . . . . 7
⊢
(∃𝑥𝑅 ∈ ( 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 276 |
. . . . . 6
⊢
((∃𝑥𝑅 ∈ ( 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 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝑅 ∈ ( 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 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 4158 |
. . 3
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 7406 |
. 2
⊢ ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( 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 2790 |
1
⊢ (𝜑 → (𝐴 ·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 𝑧𝐿)))})))) |