Proof of Theorem precsexlemcbv
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | precsexlem.1 | . 2
⊢ 𝐹 = rec((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉) | 
| 2 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑞 → (1st ‘𝑝) = (1st ‘𝑞)) | 
| 3 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞)) | 
| 4 | 3 | csbeq1d 3902 | . . . . . 6
⊢ (𝑝 = 𝑞 → ⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(2nd ‘𝑞) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉) | 
| 5 | 2, 4 | csbeq12dv 3907 | . . . . 5
⊢ (𝑝 = 𝑞 → ⦋(1st
‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(1st ‘𝑞) / 𝑙⦌⦋(2nd
‘𝑞) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉) | 
| 6 |  | rexeq 3321 | . . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑠 → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) | 
| 7 | 6 | rexbidv 3178 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) | 
| 8 | 7 | abbidv 2807 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)} =
{𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) | 
| 9 | 8 | uneq2d 4167 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) | 
| 10 | 9 | uneq2d 4167 | . . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) =
(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}))) | 
| 11 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) | 
| 12 |  | rexeq 3321 | . . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑠 → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) | 
| 13 | 12 | rexbidv 3178 | . . . . . . . . . . . . 13
⊢ (𝑟 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) | 
| 14 | 13 | abbidv 2807 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈
𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) | 
| 15 | 14 | uneq2d 4167 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) =
({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) | 
| 16 | 11, 15 | uneq12d 4168 | . . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) =
(𝑠 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))) | 
| 17 | 10, 16 | opeq12d 4880 | . . . . . . . . 9
⊢ (𝑟 = 𝑠 → 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 = 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑠 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉) | 
| 18 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ 𝑏 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝑅))) | 
| 19 | 18 | 2rexbidv 3221 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅))) | 
| 20 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑅 = 𝑧𝑅 →
(𝑥𝑅
-s 𝐴) = (𝑧𝑅
-s 𝐴)) | 
| 21 | 20 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑅 = 𝑧𝑅 →
((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿) = ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) | 
| 22 | 21 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥𝑅 = 𝑧𝑅 → (
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = (
1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿))) | 
| 23 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥𝑅 = 𝑧𝑅 →
𝑥𝑅 =
𝑧𝑅) | 
| 24 | 22, 23 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑥𝑅 = 𝑧𝑅 → ((
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝑅) = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝑅)) | 
| 25 | 24 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑥𝑅 = 𝑧𝑅 →
(𝑏 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝑅) ↔ 𝑏 = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝑅))) | 
| 26 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦𝐿 = 𝑤 → ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝑅
-s 𝐴)
·s 𝑤)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦𝐿 = 𝑤 → ( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) = (
1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤))) | 
| 28 | 27 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝑦𝐿 = 𝑤 → (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝑅) = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)) | 
| 29 | 28 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑦𝐿 = 𝑤 → (𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑧𝑅)
↔ 𝑏 = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅))) | 
| 30 | 25, 29 | cbvrex2vw 3241 | . . . . . . . . . . . . . 14
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)) | 
| 31 | 19, 30 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅))) | 
| 32 | 31 | cbvabv 2811 | . . . . . . . . . . . 12
⊢ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)} =
{𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} | 
| 33 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ 𝑏 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿))) | 
| 34 | 33 | 2rexbidv 3221 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) | 
| 35 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝐿 = 𝑧𝐿 →
(𝑥𝐿
-s 𝐴) = (𝑧𝐿
-s 𝐴)) | 
| 36 | 35 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝐿 = 𝑧𝐿 →
((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅) = ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) | 
| 37 | 36 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝐿 = 𝑧𝐿 → (
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = (
1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅))) | 
| 38 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝐿 = 𝑧𝐿 →
𝑥𝐿 =
𝑧𝐿) | 
| 39 | 37, 38 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥𝐿 = 𝑧𝐿 → ((
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿) = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝐿)) | 
| 40 | 39 | eqeq2d 2747 | . . . . . . . . . . . . . . . 16
⊢ (𝑥𝐿 = 𝑧𝐿 →
(𝑏 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿) ↔ 𝑏 = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝐿))) | 
| 41 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦𝑅 = 𝑡 → ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝐿
-s 𝐴)
·s 𝑡)) | 
| 42 | 41 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦𝑅 = 𝑡 → ( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) = (
1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡))) | 
| 43 | 42 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦𝑅 = 𝑡 → (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝐿) = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)) | 
| 44 | 43 | eqeq2d 2747 | . . . . . . . . . . . . . . . 16
⊢ (𝑦𝑅 = 𝑡 → (𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑧𝐿)
↔ 𝑏 = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿))) | 
| 45 | 40, 44 | cbvrex2vw 3241 | . . . . . . . . . . . . . . 15
⊢
(∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)) | 
| 46 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ( 0s <s 𝑥 ↔ 0s <s
𝑧)) | 
| 47 | 46 | cbvrabv 3446 | . . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} = {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧} | 
| 48 | 47 | rexeqi 3324 | . . . . . . . . . . . . . . 15
⊢
(∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)) | 
| 49 | 45, 48 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)) | 
| 50 | 34, 49 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿))) | 
| 51 | 50 | cbvabv 2811 | . . . . . . . . . . . 12
⊢ {𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)} =
{𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)} | 
| 52 | 32, 51 | uneq12i 4165 | . . . . . . . . . . 11
⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) =
({𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)}) | 
| 53 | 52 | uneq2i 4164 | . . . . . . . . . 10
⊢ (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) =
(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})) | 
| 54 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ 𝑏 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿))) | 
| 55 | 54 | 2rexbidv 3221 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿))) | 
| 56 | 35 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝐿 = 𝑧𝐿 →
((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿) = ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) | 
| 57 | 56 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝐿 = 𝑧𝐿 → (
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = (
1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿))) | 
| 58 | 57, 38 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥𝐿 = 𝑧𝐿 → ((
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿) = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝐿)) | 
| 59 | 58 | eqeq2d 2747 | . . . . . . . . . . . . . . . 16
⊢ (𝑥𝐿 = 𝑧𝐿 →
(𝑏 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿) ↔ 𝑏 = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝐿))) | 
| 60 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦𝐿 = 𝑤 → ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝐿
-s 𝐴)
·s 𝑤)) | 
| 61 | 60 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦𝐿 = 𝑤 → ( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) = (
1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤))) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦𝐿 = 𝑤 → (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑧𝐿) = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)) | 
| 63 | 62 | eqeq2d 2747 | . . . . . . . . . . . . . . . 16
⊢ (𝑦𝐿 = 𝑤 → (𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑧𝐿)
↔ 𝑏 = (( 1s
+s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿))) | 
| 64 | 59, 63 | cbvrex2vw 3241 | . . . . . . . . . . . . . . 15
⊢
(∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)) | 
| 65 | 47 | rexeqi 3324 | . . . . . . . . . . . . . . 15
⊢
(∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)) | 
| 66 | 64, 65 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)) | 
| 67 | 55, 66 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿))) | 
| 68 | 67 | cbvabv 2811 | . . . . . . . . . . . 12
⊢ {𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)} =
{𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} | 
| 69 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ 𝑏 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅))) | 
| 70 | 69 | 2rexbidv 3221 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) | 
| 71 | 20 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑅 = 𝑧𝑅 →
((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅) = ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) | 
| 72 | 71 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥𝑅 = 𝑧𝑅 → (
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = (
1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅))) | 
| 73 | 72, 23 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑥𝑅 = 𝑧𝑅 → ((
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅) = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝑅)) | 
| 74 | 73 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑥𝑅 = 𝑧𝑅 →
(𝑏 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅) ↔ 𝑏 = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝑅))) | 
| 75 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦𝑅 = 𝑡 → ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝑅
-s 𝐴)
·s 𝑡)) | 
| 76 | 75 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦𝑅 = 𝑡 → ( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) = (
1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡))) | 
| 77 | 76 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝑦𝑅 = 𝑡 → (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑧𝑅) = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)) | 
| 78 | 77 | eqeq2d 2747 | . . . . . . . . . . . . . . 15
⊢ (𝑦𝑅 = 𝑡 → (𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑧𝑅)
↔ 𝑏 = (( 1s
+s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅))) | 
| 79 | 74, 78 | cbvrex2vw 3241 | . . . . . . . . . . . . . 14
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)) | 
| 80 | 70, 79 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅))) | 
| 81 | 80 | cbvabv 2811 | . . . . . . . . . . . 12
⊢ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈
𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)} =
{𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)} | 
| 82 | 68, 81 | uneq12i 4165 | . . . . . . . . . . 11
⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) =
({𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}) | 
| 83 | 82 | uneq2i 4164 | . . . . . . . . . 10
⊢ (𝑠 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) =
(𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)})) | 
| 84 | 53, 83 | opeq12i 4877 | . . . . . . . . 9
⊢
〈(𝑙 ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑠 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 = 〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 | 
| 85 | 17, 84 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑟 = 𝑠 → 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 = 〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) | 
| 86 | 85 | cbvcsbv 3910 | . . . . . . 7
⊢
⦋(2nd ‘𝑞) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(2nd ‘𝑞) / 𝑠⦌〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 | 
| 87 | 86 | csbeq2i 3906 | . . . . . 6
⊢
⦋(1st ‘𝑞) / 𝑙⦌⦋(2nd
‘𝑞) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(1st ‘𝑞) / 𝑙⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 | 
| 88 |  | id 22 | . . . . . . . . . 10
⊢ (𝑙 = 𝑚 → 𝑙 = 𝑚) | 
| 89 |  | rexeq 3321 | . . . . . . . . . . . . 13
⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅))) | 
| 90 | 89 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → (∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅))) | 
| 91 | 90 | abbidv 2807 | . . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} = {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)}) | 
| 92 | 91 | uneq1d 4166 | . . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)}) = ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})) | 
| 93 | 88, 92 | uneq12d 4168 | . . . . . . . . 9
⊢ (𝑙 = 𝑚 → (𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})) = (𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)}))) | 
| 94 |  | rexeq 3321 | . . . . . . . . . . . . 13
⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿))) | 
| 95 | 94 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑙 = 𝑚 → (∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿))) | 
| 96 | 95 | abbidv 2807 | . . . . . . . . . . 11
⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} = {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)}) | 
| 97 | 96 | uneq1d 4166 | . . . . . . . . . 10
⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}) = ({𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)})) | 
| 98 | 97 | uneq2d 4167 | . . . . . . . . 9
⊢ (𝑙 = 𝑚 → (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)})) = (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))) | 
| 99 | 93, 98 | opeq12d 4880 | . . . . . . . 8
⊢ (𝑙 = 𝑚 → 〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 = 〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) | 
| 100 | 99 | csbeq2dv 3905 | . . . . . . 7
⊢ (𝑙 = 𝑚 → ⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 =
⦋(2nd ‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) | 
| 101 | 100 | cbvcsbv 3910 | . . . . . 6
⊢
⦋(1st ‘𝑞) / 𝑙⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 =
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 | 
| 102 | 87, 101 | eqtri 2764 | . . . . 5
⊢
⦋(1st ‘𝑞) / 𝑙⦌⦋(2nd
‘𝑞) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉 | 
| 103 | 5, 102 | eqtrdi 2792 | . . . 4
⊢ (𝑝 = 𝑞 → ⦋(1st
‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉 =
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) | 
| 104 | 103 | cbvmptv 5254 | . . 3
⊢ (𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉) = (𝑞 ∈ V ↦
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) | 
| 105 |  | rdgeq1 8452 | . . 3
⊢ ((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉) = (𝑞 ∈ V ↦
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉) →
rec((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉) = rec((𝑞 ∈ V ↦
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉), 〈{
0s }, ∅〉)) | 
| 106 | 104, 105 | ax-mp 5 | . 2
⊢
rec((𝑝 ∈ V
↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉) = rec((𝑞 ∈ V ↦
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉), 〈{
0s }, ∅〉) | 
| 107 | 1, 106 | eqtri 2764 | 1
⊢ 𝐹 = rec((𝑞 ∈ V ↦
⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd
‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑤))
/su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈
{𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑡))
/su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s
𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿
-s 𝐴)
·s 𝑤))
/su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R
‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅
-s 𝐴)
·s 𝑡))
/su 𝑧𝑅)}))〉), 〈{
0s }, ∅〉) |