precsexlemcbv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > precsexlemcbv		Structured version Visualization version GIF version

Theorem precsexlemcbv 28592

Description: Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.)

**Hypothesis**
Ref	Expression
precsexlem.1	⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)

**Assertion**
Ref	Expression
precsexlemcbv	⊢ 𝐹 = rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)

Distinct variable group: 𝐴,𝑝,𝑞,𝑙,𝑚,𝑟,𝑠,𝑎,𝑏,𝑥_𝐿,𝑥_𝑅,𝑧_𝐿,𝑧_𝑅,𝑦_𝐿,𝑦_𝑅,𝑤,𝑡,𝑥,𝑧 Allowed substitution hints: 𝐹(𝑥, 𝑧, 𝑤, 𝑡, 𝑚, 𝑠, 𝑟, 𝑞, 𝑝, 𝑎, 𝑏, 𝑙, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅, 𝑧_𝐿, 𝑧_𝑅)

**Proof of Theorem precsexlemcbv**
Step	Hyp	Ref	Expression
1		precsexlem.1	. 2 ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
2		fveq2 6885	. . . . . 6 ⊢ (𝑝 = 𝑞 → (1^st ‘𝑝) = (1^st ‘𝑞))
3		fveq2 6885	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
4	3	csbeq1d 3850	. . . . . 6 ⊢ (𝑝 = 𝑞 → ⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(2^nd ‘𝑞) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩)
5	2, 4	csbeq12dv 3855	. . . . 5 ⊢ (𝑝 = 𝑞 → ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(1^st ‘𝑞) / 𝑙⦌⦋(2^nd ‘𝑞) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩)
6		rexeq 3315	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → (∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)))
7	6	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑠 → (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)))
8	7	abbidv 2826	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)} = {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})
9	8	uneq2d 4167	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)}) = ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)}))
10	9	uneq2d 4167	. . . . . . . . . 10 ⊢ (𝑟 = 𝑠 → (𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})) = (𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})))
11		id 23	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠)
12		rexeq 3315	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → (∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ ∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)))
13	12	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑠 → (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)))
14	13	abbidv 2826	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)} = {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})
15	14	uneq2d 4167	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}) = ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))
16	11, 15	uneq12d 4168	. . . . . . . . . 10 ⊢ (𝑟 = 𝑠 → (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})) = (𝑠 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})))
17	10, 16	opeq12d 4840	. . . . . . . . 9 ⊢ (𝑟 = 𝑠 → ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑠 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩)
18		eqeq1 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)))
19	18	2rexbidv 3227	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ↔ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)))
20		oveq1 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → (𝑥_𝑅 −_s 𝐴) = (𝑧_𝑅 −_s 𝐴))
21	20	oveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿) = ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿))
22	21	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → ( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) = ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)))
23		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → 𝑥_𝑅 = 𝑧_𝑅)
24	22, 23	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝑅))
25	24	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → (𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝑅)))
26		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦_𝐿 = 𝑤 → ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿) = ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤))
27	26	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦_𝐿 = 𝑤 → ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) = ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)))
28	27	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦_𝐿 = 𝑤 → (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝑅) = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅))
29	28	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑦_𝐿 = 𝑤 → (𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)))
30	25, 29	cbvrex2vw 3245	. . . . . . . . . . . . . 14 ⊢ (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ↔ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅))
31	19, 30	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ↔ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)))
32	31	cbvabv 2830	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} = {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)}
33		eqeq1 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)))
34	33	2rexbidv 3227	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)))
35		oveq1 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → (𝑥_𝐿 −_s 𝐴) = (𝑧_𝐿 −_s 𝐴))
36	35	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅) = ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅))
37	36	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → ( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) = ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)))
38		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → 𝑥_𝐿 = 𝑧_𝐿)
39	37, 38	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝐿))
40	39	eqeq2d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → (𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝐿)))
41		oveq2 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦_𝑅 = 𝑡 → ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅) = ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡))
42	41	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦_𝑅 = 𝑡 → ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) = ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)))
43	42	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦_𝑅 = 𝑡 → (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝐿) = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿))
44	43	eqeq2d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑦_𝑅 = 𝑡 → (𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)))
45	40, 44	cbvrex2vw 3245	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿))
46		breq2 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ( 0_s <s 𝑥 ↔ 0_s <s 𝑧))
47	46	cbvrabv 3422	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥} = {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}
48	47	rexeqi 3318	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿))
49	45, 48	bitri 278	. . . . . . . . . . . . . 14 ⊢ (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿))
50	34, 49	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)))
51	50	cbvabv 2830	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)} = {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)}
52	32, 51	uneq12i 4165	. . . . . . . . . . 11 ⊢ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)}) = ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})
53	52	uneq2i 4164	. . . . . . . . . 10 ⊢ (𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})) = (𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)}))
54		eqeq1 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)))
55	54	2rexbidv 3227	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)))
56	35	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿) = ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿))
57	56	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → ( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) = ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)))
58	57, 38	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝐿))
59	58	eqeq2d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝐿 = 𝑧_𝐿 → (𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝐿)))
60		oveq2 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦_𝐿 = 𝑤 → ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿) = ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤))
61	60	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦_𝐿 = 𝑤 → ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) = ( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)))
62	61	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦_𝐿 = 𝑤 → (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝐿) = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿))
63	62	eqeq2d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑦_𝐿 = 𝑤 → (𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑧_𝐿) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)))
64	59, 63	cbvrex2vw 3245	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿))
65	47	rexeqi 3318	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿))
66	64, 65	bitri 278	. . . . . . . . . . . . . 14 ⊢ (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿))
67	55, 66	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)))
68	67	cbvabv 2830	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} = {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)}
69		eqeq1 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)))
70	69	2rexbidv 3227	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)))
71	20	oveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅) = ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅))
72	71	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → ( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) = ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)))
73	72, 23	oveq12d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝑅))
74	73	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑥_𝑅 = 𝑧_𝑅 → (𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝑅)))
75		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦_𝑅 = 𝑡 → ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅) = ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡))
76	75	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦_𝑅 = 𝑡 → ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) = ( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)))
77	76	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦_𝑅 = 𝑡 → (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝑅) = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅))
78	77	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑦_𝑅 = 𝑡 → (𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑧_𝑅) ↔ 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)))
79	74, 78	cbvrex2vw 3245	. . . . . . . . . . . . . 14 ⊢ (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅))
80	70, 79	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ↔ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)))
81	80	cbvabv 2830	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)} = {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}
82	68, 81	uneq12i 4165	. . . . . . . . . . 11 ⊢ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}) = ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)})
83	82	uneq2i 4164	. . . . . . . . . 10 ⊢ (𝑠 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})) = (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))
84	53, 83	opeq12i 4837	. . . . . . . . 9 ⊢ ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑠 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑠 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩
85	17, 84	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑟 = 𝑠 → ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩)
86	85	cbvcsbv 3858	. . . . . . 7 ⊢ ⦋(2^nd ‘𝑞) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩
87	86	csbeq2i 3854	. . . . . 6 ⊢ ⦋(1^st ‘𝑞) / 𝑙⦌⦋(2^nd ‘𝑞) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(1^st ‘𝑞) / 𝑙⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩
88		id 23	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → 𝑙 = 𝑚)
89		rexeq 3315	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)))
90	89	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑚 → (∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅) ↔ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)))
91	90	abbidv 2826	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} = {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)})
92	91	uneq1d 4166	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)}) = ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)}))
93	88, 92	uneq12d 4168	. . . . . . . . 9 ⊢ (𝑙 = 𝑚 → (𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})) = (𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})))
94		rexeq 3315	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)))
95	94	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑚 → (∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿) ↔ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)))
96	95	abbidv 2826	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} = {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)})
97	96	uneq1d 4166	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}) = ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))
98	97	uneq2d 4167	. . . . . . . . 9 ⊢ (𝑙 = 𝑚 → (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)})) = (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)})))
99	93, 98	opeq12d 4840	. . . . . . . 8 ⊢ (𝑙 = 𝑚 → ⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩ = ⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩)
100	99	csbeq2dv 3853	. . . . . . 7 ⊢ (𝑙 = 𝑚 → ⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩ = ⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩)
101	100	cbvcsbv 3858	. . . . . 6 ⊢ ⦋(1^st ‘𝑞) / 𝑙⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩ = ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩
102	87, 101	eqtri 2783	. . . . 5 ⊢ ⦋(1^st ‘𝑞) / 𝑙⦌⦋(2^nd ‘𝑞) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩
103	5, 102	eqtrdi 2811	. . . 4 ⊢ (𝑝 = 𝑞 → ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩ = ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩)
104	103	cbvmptv 5208	. . 3 ⊢ (𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩) = (𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩)
105		rdgeq1 8419	. . 3 ⊢ ((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩) = (𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩) → rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩) = rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩))
106	104, 105	ax-mp 5	. 2 ⊢ rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 −_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ (R‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 −_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩) = rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
107	1, 106	eqtri 2783	1 ⊢ 𝐹 = rec((𝑞 ∈ V ↦ ⦋(1^st ‘𝑞) / 𝑚⦌⦋(2^nd ‘𝑞) / 𝑠⦌⟨(𝑚 ∪ ({𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝑅)} ∪ {𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧_𝐿 ∈ {𝑧 ∈ (L‘𝐴) ∣ 0_s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1_s +_s ((𝑧_𝐿 −_s 𝐴) ·_s 𝑤)) /_su 𝑧_𝐿)} ∪ {𝑏 ∣ ∃𝑧_𝑅 ∈ (R‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1_s +_s ((𝑧_𝑅 −_s 𝐴) ·_s 𝑡)) /_su 𝑧_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1569 {cab 2738 ∃wrex 3086 {crab 3412 Vcvv 3450 ⦋csb 3846 ∪ cun 4149 ∅c0 4278 {csn 4583 ⟨cop 4589 class class class wbr 5102 ↦ cmpt 5185 ‘cfv 6538 (class class class)co 7420 1^st c1st 7999 2^nd c2nd 8000 reccrdg 8417 <s clts 27998 0_s c0s 28191 1_s c1s 28192 Lcleft 28211 Rcright 28212 +_s cadds 28345 −_s csubs 28406 ·_s cmuls 28492 /_su cdivs 28573

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-xp 5656 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-iota 6494 df-fv 6546 df-ov 7423 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418

This theorem is used by: precsex 28604

W3C validator