| Step | Hyp | Ref
| Expression |
| 1 | | mulsasslem.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ No
) |
| 2 | | mulsasslem.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ No
) |
| 3 | 1, 2 | mulscut2 28159 |
. . 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 27911 |
. . . 4
⊢ ( L
‘𝐶) <<s ( R
‘𝐶) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → ( L ‘𝐶) <<s ( R ‘𝐶)) |
| 6 | | mulsval2 28137 |
. . . 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 27941 |
. . . . 5
⊢ (𝐶 ∈
No → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
| 10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
| 11 | 10 | eqcomd 2743 |
. . 3
⊢ (𝜑 → 𝐶 = (( L ‘𝐶) |s ( R ‘𝐶))) |
| 12 | 3, 5, 7, 11 | mulsunif 28176 |
. 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 4308 |
. . . . 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 4196 |
. . . . . . 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 2741 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
↔ 𝑡 = (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)))) |
| 16 | 15 | 2rexbidv 3222 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿)))) |
| 17 | 16 | rexab 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7464 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ∈
V |
| 21 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝐶) =
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶)) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
| 23 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝐿)) |
| 24 | 22, 23 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 2741 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
↔ 𝑡 = (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)))) |
| 36 | 35 | 2rexbidv 3222 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅)))) |
| 37 | 36 | rexab 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7464 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ∈
V |
| 41 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝐶) =
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶)) |
| 42 | 41 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
| 43 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝐿)) |
| 44 | 42, 43 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 915 |
. . . . . . 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 276 |
. . . . . 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 2809 |
. . . . 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 2765 |
. . . 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 4308 |
. . . . 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 4196 |
. . . . . . 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 2741 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
↔ 𝑡 = (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)))) |
| 62 | 61 | 2rexbidv 3222 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑏 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)∃𝑦𝑅 ∈ ( R ‘𝐵)𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅)))) |
| 63 | 62 | rexab 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7464 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ∈
V |
| 67 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝐶) =
((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶)) |
| 68 | 67 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
| 69 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝑅)) |
| 70 | 68, 69 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 2741 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑡 → (𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
↔ 𝑡 = (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)))) |
| 82 | 81 | 2rexbidv 3222 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑡 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑏 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ ( L ‘𝐵)𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿)))) |
| 83 | 82 | rexab 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7464 |
. . . . . . . . . . . . . 14
⊢ (((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ∈
V |
| 87 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝐶) =
((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶)) |
| 88 | 87 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
| 89 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝑅)) |
| 90 | 88, 89 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 915 |
. . . . . . 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 276 |
. . . . . 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 2809 |
. . . . 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 2765 |
. . . 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 4166 |
. . 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 4308 |
. . . . 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 4196 |
. . . . . . 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 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
| 112 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝐿 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝐿
·s 𝑦𝐿)) ·s
𝑧𝑅)) |
| 113 | 111, 112 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝑅)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝑅))) |
| 128 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝑅 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝑅) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝑅
·s 𝑦𝑅)) ·s
𝑧𝑅)) |
| 129 | 127, 128 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 915 |
. . . . . . 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 276 |
. . . . . 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 2809 |
. . . . 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 2765 |
. . . 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 4308 |
. . . . 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 4196 |
. . . . . . 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 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
| 150 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝐿 ·s
𝐵) +s (𝐴 ·s 𝑦𝑅))
-s (𝑥𝐿 ·s
𝑦𝑅))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝐿
·s 𝐵)
+s (𝐴
·s 𝑦𝑅)) -s (𝑥𝐿
·s 𝑦𝑅)) ·s
𝑧𝐿)) |
| 151 | 149, 150 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 3700 |
. . . . . . . . 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 3288 |
. . . . . . . . . 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 3288 |
. . . . . . . . . . . 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 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ ((𝑡
·s 𝐶)
+s ((𝐴
·s 𝐵)
·s 𝑧𝐿)) = (((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝐶) +s ((𝐴 ·s 𝐵) ·s 𝑧𝐿))) |
| 166 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝑥𝑅 ·s
𝐵) +s (𝐴 ·s 𝑦𝐿))
-s (𝑥𝑅 ·s
𝑦𝐿))
→ (𝑡
·s 𝑧𝐿) = ((((𝑥𝑅
·s 𝐵)
+s (𝐴
·s 𝑦𝐿)) -s (𝑥𝑅
·s 𝑦𝐿)) ·s
𝑧𝐿)) |
| 167 | 165, 166 | oveq12d 7449 |
. . . . . . . . . . . . . . . 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 2748 |
. . . . . . . . . . . . . . 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 3179 |
. . . . . . . . . . . . . 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 3532 |
. . . . . . . . . . . . 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 277 |
. . . . . . . . . . 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 3227 |
. . . . . . . . . . 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 1848 |
. . . . . . . . . 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 302 |
. . . . . . . . 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 275 |
. . . . . . . 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 915 |
. . . . . . 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 276 |
. . . . . 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 2809 |
. . . . 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 2765 |
. . . 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 4166 |
. . 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 7443 |
. 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 2795 |
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
𝑧𝐿))})))) |