Step | Hyp | Ref
| Expression |
1 | | mulsasslem.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | mulsasslem.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | 1, 2 | mulscut2 27518 |
. . 3
⊢ (𝜑 → ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})
<<s ({𝑏 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})) |
4 | | lltropt 27296 |
. . . 4
⊢ ( L
‘𝐶) <<s ( R
‘𝐶) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → ( L ‘𝐶) <<s ( R ‘𝐶)) |
6 | | mulsval2 27496 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ·s 𝐵) = (({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})
|s ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}))) |
7 | 1, 2, 6 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐴 ·s 𝐵) = (({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})
|s ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}))) |
8 | | mulsasslem.3 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ No
) |
9 | | lrcut 27326 |
. . . . 5
⊢ (𝐶 ∈
No → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
11 | 10 | eqcomd 2738 |
. . 3
⊢ (𝜑 → 𝐶 = (( L ‘𝐶) |s ( R ‘𝐶))) |
12 | 3, 5, 7, 11 | mulsunif 27534 |
. 2
⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = (({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))}) |s
({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))}))) |
13 | | unab 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))}) =
{𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))} |
14 | | rexun 4187 |
. . . . . . 7
⊢
(∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
(∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
15 | | eqeq1 2736 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
↔ 𝑡 = (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)))) |
16 | 15 | 2rexbidv 3219 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿)))) |
17 | 16 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
18 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
19 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
20 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ∈
V |
21 | | oveq1 7401 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝐶) =
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶)) |
22 | 21 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
23 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿)) |
24 | 22, 23 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) =
((((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s ((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧𝐿))) |
25 | 24 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s (𝑡
·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿)))) |
26 | 25 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿)))) |
27 | 20, 26 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
28 | 27 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
29 | 19, 28 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
30 | 29 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
31 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
32 | 31 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
33 | 18, 30, 32 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
34 | 17, 33 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
35 | | eqeq1 2736 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
↔ 𝑡 = (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)))) |
36 | 35 | 2rexbidv 3219 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅)))) |
37 | 36 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
38 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
39 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
40 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ∈
V |
41 | | oveq1 7401 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝐶) =
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶)) |
42 | 41 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
43 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)) |
44 | 42, 43 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) =
((((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s ((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧𝐿))) |
45 | 44 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s (𝑡
·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))) |
46 | 45 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))) |
47 | 40, 46 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
48 | 47 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
49 | 39, 48 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
50 | 49 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
51 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
52 | 51 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
53 | 38, 50, 52 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
54 | 37, 53 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
55 | 34, 54 | orbi12i 913 |
. . . . . . 7
⊢
((∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))) |
56 | 14, 55 | bitr2i 275 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))
↔ ∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) |
57 | 56 | abbii 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)))} =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} |
58 | 13, 57 | eqtri 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))}) =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} |
59 | | unab 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}) =
{𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))} |
60 | | rexun 4187 |
. . . . . . 7
⊢
(∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
(∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
61 | | eqeq1 2736 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
↔ 𝑡 = (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)))) |
62 | 61 | 2rexbidv 3219 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅)))) |
63 | 62 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
64 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
65 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
66 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ∈
V |
67 | | oveq1 7401 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝐶) =
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶)) |
68 | 67 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
69 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅)) |
70 | 68, 69 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) =
((((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s ((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧𝑅))) |
71 | 70 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s (𝑡
·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅)))) |
72 | 71 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅)))) |
73 | 66, 72 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
74 | 73 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
75 | 65, 74 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
76 | 75 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
77 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
78 | 77 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
79 | 64, 76, 78 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
80 | 63, 79 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
81 | | eqeq1 2736 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
↔ 𝑡 = (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)))) |
82 | 81 | 2rexbidv 3219 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿)))) |
83 | 82 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
84 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
85 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
86 | | ovex 7427 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ∈
V |
87 | | oveq1 7401 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝐶) =
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶)) |
88 | 87 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
89 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)) |
90 | 88, 89 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) =
((((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s ((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧𝑅))) |
91 | 90 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s (𝑡
·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))) |
92 | 91 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))) |
93 | 86, 92 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
94 | 93 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
95 | 85, 94 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
96 | 95 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
97 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
98 | 97 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
99 | 84, 96, 98 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
100 | 83, 99 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
101 | 80, 100 | orbi12i 913 |
. . . . . . 7
⊢
((∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))) |
102 | 60, 101 | bitr2i 275 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))
↔ ∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) |
103 | 102 | abbii 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)))} =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} |
104 | 59, 103 | eqtri 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}) =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} |
105 | 58, 104 | uneq12i 4158 |
. . 3
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
= ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))}) |
106 | | unab 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))}) =
{𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))} |
107 | | rexun 4187 |
. . . . . . 7
⊢
(∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
(∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
108 | 16 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
109 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
110 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
111 | 21 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
112 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅)) |
113 | 111, 112 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) =
((((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s ((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝑧𝑅))) |
114 | 113 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s (𝑡
·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅)))) |
115 | 114 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅)))) |
116 | 20, 115 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
117 | 116 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
118 | 110, 117 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
119 | 118 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
120 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
121 | 120 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
122 | 109, 119,
121 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
123 | 108, 122 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))) |
124 | 36 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
125 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
126 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
127 | 41 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
128 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)) |
129 | 127, 128 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) =
((((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s ((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝑧𝑅))) |
130 | 129 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))
-s (𝑡
·s 𝑧𝑅)) ↔ 𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))) |
131 | 130 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))) |
132 | 40, 131 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
133 | 132 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
134 | 126, 133 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
135 | 134 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
136 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
137 | 136 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)))) |
138 | 125, 135,
137 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
∧ ∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
139 | 124, 138 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))) |
140 | 123, 139 | orbi12i 913 |
. . . . . . 7
⊢
((∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))}∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))) |
141 | 107, 140 | bitr2i 275 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))
↔ ∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))) |
142 | 141 | abbii 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)))} =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} |
143 | 106, 142 | eqtri 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))}) =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} |
144 | | unab 4295 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}) =
{𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))} |
145 | | rexun 4187 |
. . . . . . 7
⊢
(∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
(∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
146 | 62 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
147 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
148 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑦𝑅 ∈ ( R
‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
149 | 67 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
150 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿)) |
151 | 149, 150 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) =
((((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s ((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝑧𝐿))) |
152 | 151 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s (𝑡
·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿)))) |
153 | 152 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿)))) |
154 | 66, 153 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
155 | 154 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑡(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
156 | 148, 155 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
157 | 156 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑡∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
158 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
159 | 158 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)(𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡(∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
160 | 147, 157,
159 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
161 | 146, 160 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))) |
162 | 82 | rexab 3687 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
163 | | rexcom4 3285 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
164 | | rexcom4 3285 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡∃𝑦𝐿 ∈ ( L
‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
165 | 87 | oveq1d 7409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
166 | | oveq1 7401 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)) |
167 | 165, 166 | oveq12d 7412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) =
((((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s ((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝑧𝐿))) |
168 | 167 | eqeq2d 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))
-s (𝑡
·s 𝑧𝐿)) ↔ 𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))) |
169 | 168 | rexbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))) |
170 | 86, 169 | ceqsexv 3523 |
. . . . . . . . . . . . 13
⊢
(∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
171 | 170 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑡(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
172 | 164, 171 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑦𝐿
∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
173 | 172 | rexbii 3094 |
. . . . . . . . . 10
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑡∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
174 | | r19.41vv 3224 |
. . . . . . . . . . 11
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
175 | 174 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑡∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)(𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑡(∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)))) |
176 | 163, 173,
175 | 3bitr3ri 301 |
. . . . . . . . 9
⊢
(∃𝑡(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
∧ ∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
177 | 162, 176 | bitri 274 |
. . . . . . . 8
⊢
(∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))) |
178 | 161, 177 | orbi12i 913 |
. . . . . . 7
⊢
((∃𝑡 ∈
{𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿)) ∨
∃𝑡 ∈ {𝑏 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))}∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) ↔
(∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))) |
179 | 145, 178 | bitr2i 275 |
. . . . . 6
⊢
((∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))
↔ ∃𝑡 ∈
({𝑏 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))) |
180 | 179 | abbii 2802 |
. . . . 5
⊢ {𝑎 ∣ (∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))
∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)))} =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} |
181 | 144, 180 | eqtri 2760 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝑅 ∈ ( R
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}) =
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} |
182 | 143, 181 | uneq12i 4158 |
. . 3
⊢ (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))}))
= ({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))}) |
183 | 105, 182 | oveq12i 7406 |
. 2
⊢ ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L
‘𝐴)∃𝑦𝐿 ∈ ( L
‘𝐵)∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))})))
= (({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))}) |s
({𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))})∃𝑧𝑅 ∈ ( R
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅)) -s (𝑡 ·s 𝑧𝑅))} ∪
{𝑎 ∣ ∃𝑡 ∈ ({𝑏 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))}
∪ {𝑏 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))})∃𝑧𝐿 ∈ ( L
‘𝐶)𝑎 = (((𝑡 ·s 𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿)) -s (𝑡 ·s 𝑧𝐿))})) |
184 | 12, 183 | eqtr4di 2790 |
1
⊢ (𝜑 → ((𝐴 ·s 𝐵) ·s 𝐶) = ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅))}))
|s (({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝑅 ∈ ( R ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅))})
∪ ({𝑎 ∣
∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿))}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)∃𝑧𝐿 ∈ ( L ‘𝐶)𝑎 = ((((((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) -s
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿))})))) |