| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢ (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) = (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) | 
| 2 | 1 | rnmpo 7567 | . . . 4
⊢ ran
(𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) = {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} | 
| 3 |  | ssltmul1.1 | . . . . . . 7
⊢ (𝜑 → 𝐿 <<s 𝑅) | 
| 4 |  | ssltex1 27832 | . . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) | 
| 5 | 3, 4 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐿 ∈ V) | 
| 6 |  | ssltmul1.2 | . . . . . . 7
⊢ (𝜑 → 𝑀 <<s 𝑆) | 
| 7 |  | ssltex1 27832 | . . . . . . 7
⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V) | 
| 8 | 6, 7 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ V) | 
| 9 | 1 | mpoexg 8102 | . . . . . 6
⊢ ((𝐿 ∈ V ∧ 𝑀 ∈ V) → (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) | 
| 10 | 5, 8, 9 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) | 
| 11 |  | rnexg 7925 | . . . . 5
⊢ ((𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V → ran (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) | 
| 12 | 10, 11 | syl 17 | . . . 4
⊢ (𝜑 → ran (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) | 
| 13 | 2, 12 | eqeltrrid 2845 | . . 3
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∈ V) | 
| 14 |  | eqid 2736 | . . . . 5
⊢ (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) = (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) | 
| 15 | 14 | rnmpo 7567 | . . . 4
⊢ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) = {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} | 
| 16 |  | ssltex2 27833 | . . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) | 
| 17 | 3, 16 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ V) | 
| 18 |  | ssltex2 27833 | . . . . . . 7
⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V) | 
| 19 | 6, 18 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) | 
| 20 | 14 | mpoexg 8102 | . . . . . 6
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) | 
| 21 | 17, 19, 20 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) | 
| 22 |  | rnexg 7925 | . . . . 5
⊢ ((𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V → ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) | 
| 23 | 21, 22 | syl 17 | . . . 4
⊢ (𝜑 → ran (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) | 
| 24 | 15, 23 | eqeltrrid 2845 | . . 3
⊢ (𝜑 → {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ∈ V) | 
| 25 | 13, 24 | unexd 7775 | . 2
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ∈ V) | 
| 26 |  | snex 5435 | . . 3
⊢ {(𝐴 ·s 𝐵)} ∈ V | 
| 27 | 26 | a1i 11 | . 2
⊢ (𝜑 → {(𝐴 ·s 𝐵)} ∈ V) | 
| 28 |  | ssltss1 27834 | . . . . . . . . . . . 12
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆  No
) | 
| 29 | 3, 28 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ⊆  No
) | 
| 30 | 29 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐿 ⊆  No
) | 
| 31 |  | simprl 770 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 ∈ 𝐿) | 
| 32 | 30, 31 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 ∈  No
) | 
| 33 |  | ssltmul1.4 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆)) | 
| 34 | 6 | scutcld 27849 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 |s 𝑆) ∈  No
) | 
| 35 | 33, 34 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐵 ∈  No
) | 
| 37 | 32, 36 | mulscld 28162 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝐵) ∈  No
) | 
| 38 |  | ssltmul1.3 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) | 
| 39 | 3 | scutcld 27849 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐿 |s 𝑅) ∈  No
) | 
| 40 | 38, 39 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 41 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐴 ∈  No
) | 
| 42 |  | ssltss1 27834 | . . . . . . . . . . . 12
⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆  No
) | 
| 43 | 6, 42 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ⊆  No
) | 
| 44 | 43 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑀 ⊆  No
) | 
| 45 |  | simprr 772 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 ∈ 𝑀) | 
| 46 | 44, 45 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 ∈  No
) | 
| 47 | 41, 46 | mulscld 28162 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝑞) ∈  No
) | 
| 48 | 37, 47 | addscld 28014 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) ∈  No
) | 
| 49 | 32, 46 | mulscld 28162 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝑞) ∈  No
) | 
| 50 | 48, 49 | subscld 28094 | . . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∈  No
) | 
| 51 |  | eleq1 2828 | . . . . . 6
⊢ (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → (𝑎 ∈  No 
↔ (((𝑝
·s 𝐵)
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))
∈  No )) | 
| 52 | 50, 51 | syl5ibrcom 247 | . . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑎 ∈  No
)) | 
| 53 | 52 | rexlimdvva 3212 | . . . 4
⊢ (𝜑 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑎 ∈  No
)) | 
| 54 | 53 | abssdv 4067 | . . 3
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ⊆  No
) | 
| 55 |  | ssltss2 27835 | . . . . . . . . . . . 12
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆  No
) | 
| 56 | 3, 55 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ⊆  No
) | 
| 57 | 56 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑅 ⊆  No
) | 
| 58 |  | simprl 770 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑟 ∈ 𝑅) | 
| 59 | 57, 58 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑟 ∈  No
) | 
| 60 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 ∈  No
) | 
| 61 | 59, 60 | mulscld 28162 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝐵) ∈  No
) | 
| 62 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 ∈  No
) | 
| 63 |  | ssltss2 27835 | . . . . . . . . . . . 12
⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆  No
) | 
| 64 | 6, 63 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆  No
) | 
| 65 | 64 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑆 ⊆  No
) | 
| 66 |  | simprr 772 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑠 ∈ 𝑆) | 
| 67 | 65, 66 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑠 ∈  No
) | 
| 68 | 62, 67 | mulscld 28162 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝑠) ∈  No
) | 
| 69 | 61, 68 | addscld 28014 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) ∈  No
) | 
| 70 | 59, 67 | mulscld 28162 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝑠) ∈  No
) | 
| 71 | 69, 70 | subscld 28094 | . . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ∈  No
) | 
| 72 |  | eleq1 2828 | . . . . . 6
⊢ (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → (𝑏 ∈  No 
↔ (((𝑟
·s 𝐵)
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠))
∈  No )) | 
| 73 | 71, 72 | syl5ibrcom 247 | . . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑏 ∈  No
)) | 
| 74 | 73 | rexlimdvva 3212 | . . . 4
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑏 ∈  No
)) | 
| 75 | 74 | abssdv 4067 | . . 3
⊢ (𝜑 → {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ⊆  No
) | 
| 76 | 54, 75 | unssd 4191 | . 2
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ⊆  No
) | 
| 77 | 40, 35 | mulscld 28162 | . . 3
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈  No
) | 
| 78 | 77 | snssd 4808 | . 2
⊢ (𝜑 → {(𝐴 ·s 𝐵)} ⊆  No
) | 
| 79 |  | elun 4152 | . . . . . . 7
⊢ (𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ↔ (𝑥 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∨ 𝑥 ∈ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) | 
| 80 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 81 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) | 
| 82 | 81 | 2rexbidv 3221 | . . . . . . . . 9
⊢ (𝑎 = 𝑥 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) | 
| 83 | 80, 82 | elab 3678 | . . . . . . . 8
⊢ (𝑥 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ↔ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) | 
| 84 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 85 | 84 | 2rexbidv 3221 | . . . . . . . . 9
⊢ (𝑏 = 𝑥 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 86 | 80, 85 | elab 3678 | . . . . . . . 8
⊢ (𝑥 ∈ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) | 
| 87 | 83, 86 | orbi12i 914 | . . . . . . 7
⊢ ((𝑥 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∨ 𝑥 ∈ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ↔ (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∨ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 88 | 79, 87 | bitri 275 | . . . . . 6
⊢ (𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ↔ (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∨ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) | 
| 89 | 37, 47, 49 | addsubsd 28113 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) +s (𝐴 ·s 𝑞))) | 
| 90 |  | scutcut 27847 | . . . . . . . . . . . . . . . 16
⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 91 | 3, 90 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 92 | 91 | simp2d 1143 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)}) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐿 <<s {(𝐿 |s 𝑅)}) | 
| 94 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝐿 |s 𝑅) ∈ V | 
| 95 | 94 | snid 4661 | . . . . . . . . . . . . . . 15
⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)} | 
| 96 | 38, 95 | eqeltrdi 2848 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ {(𝐿 |s 𝑅)}) | 
| 97 | 96 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐴 ∈ {(𝐿 |s 𝑅)}) | 
| 98 | 93, 31, 97 | ssltsepcd 27840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 <s 𝐴) | 
| 99 |  | scutcut 27847 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈  No 
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) | 
| 100 | 6, 99 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 |s 𝑆) ∈  No 
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) | 
| 101 | 100 | simp2d 1143 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)}) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑀 <<s {(𝑀 |s 𝑆)}) | 
| 103 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 |s 𝑆) ∈ V | 
| 104 | 103 | snid 4661 | . . . . . . . . . . . . . . 15
⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)} | 
| 105 | 33, 104 | eqeltrdi 2848 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ {(𝑀 |s 𝑆)}) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐵 ∈ {(𝑀 |s 𝑆)}) | 
| 107 | 102, 45, 106 | ssltsepcd 27840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 <s 𝐵) | 
| 108 | 32, 41, 46, 36, 98, 107 | sltmuld 28164 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑞))) | 
| 109 | 37, 49 | subscld 28094 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) ∈  No
) | 
| 110 | 77 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝐵) ∈  No
) | 
| 111 | 109, 47, 110 | sltaddsubd 28122 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) +s (𝐴 ·s 𝑞)) <s (𝐴 ·s 𝐵) ↔ ((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑞)))) | 
| 112 | 108, 111 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) +s (𝐴 ·s 𝑞)) <s (𝐴 ·s 𝐵)) | 
| 113 | 89, 112 | eqbrtrd 5164 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) <s (𝐴 ·s 𝐵)) | 
| 114 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → (𝑥 <s (𝐴 ·s 𝐵) ↔ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) <s (𝐴 ·s 𝐵))) | 
| 115 | 113, 114 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 116 | 115 | rexlimdvva 3212 | . . . . . . 7
⊢ (𝜑 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 117 | 61, 68, 70 | addsubsd 28113 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠))) | 
| 118 | 3 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐿 <<s 𝑅) | 
| 119 | 118, 90 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 120 | 119 | simp3d 1144 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {(𝐿 |s 𝑅)} <<s 𝑅) | 
| 121 | 38 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 = (𝐿 |s 𝑅)) | 
| 122 | 121, 95 | eqeltrdi 2848 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 ∈ {(𝐿 |s 𝑅)}) | 
| 123 | 120, 122,
58 | ssltsepcd 27840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 <s 𝑟) | 
| 124 | 6 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑀 <<s 𝑆) | 
| 125 | 124, 99 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑀 |s 𝑆) ∈  No 
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) | 
| 126 | 125 | simp3d 1144 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {(𝑀 |s 𝑆)} <<s 𝑆) | 
| 127 | 33 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 = (𝑀 |s 𝑆)) | 
| 128 | 127, 104 | eqeltrdi 2848 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 ∈ {(𝑀 |s 𝑆)}) | 
| 129 | 126, 128,
66 | ssltsepcd 27840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 <s 𝑠) | 
| 130 | 62, 59, 60, 67, 123, 129 | sltmuld 28164 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝑠) -s (𝐴 ·s 𝐵)) <s ((𝑟 ·s 𝑠) -s (𝑟 ·s 𝐵))) | 
| 131 | 61, 70 | subscld 28094 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) ∈  No
) | 
| 132 | 77 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝐵) ∈  No
) | 
| 133 | 131, 68, 132 | sltaddsubd 28122 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠)) <s (𝐴 ·s 𝐵) ↔ ((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑠)))) | 
| 134 | 61, 70, 132, 68 | sltsubsub2bd 28115 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑠)) ↔ ((𝐴 ·s 𝑠) -s (𝐴 ·s 𝐵)) <s ((𝑟 ·s 𝑠) -s (𝑟 ·s 𝐵)))) | 
| 135 | 133, 134 | bitrd 279 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠)) <s (𝐴 ·s 𝐵) ↔ ((𝐴 ·s 𝑠) -s (𝐴 ·s 𝐵)) <s ((𝑟 ·s 𝑠) -s (𝑟 ·s 𝐵)))) | 
| 136 | 130, 135 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠)) <s (𝐴 ·s 𝐵)) | 
| 137 | 117, 136 | eqbrtrd 5164 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) <s (𝐴 ·s 𝐵)) | 
| 138 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → (𝑥 <s (𝐴 ·s 𝐵) ↔ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) <s (𝐴 ·s 𝐵))) | 
| 139 | 137, 138 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 140 | 139 | rexlimdvva 3212 | . . . . . . 7
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 141 | 116, 140 | jaod 859 | . . . . . 6
⊢ (𝜑 → ((∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∨ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 142 | 88, 141 | biimtrid 242 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) → 𝑥 <s (𝐴 ·s 𝐵))) | 
| 143 | 142 | imp 406 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) → 𝑥 <s (𝐴 ·s 𝐵)) | 
| 144 |  | velsn 4641 | . . . . 5
⊢ (𝑦 ∈ {(𝐴 ·s 𝐵)} ↔ 𝑦 = (𝐴 ·s 𝐵)) | 
| 145 |  | breq2 5146 | . . . . 5
⊢ (𝑦 = (𝐴 ·s 𝐵) → (𝑥 <s 𝑦 ↔ 𝑥 <s (𝐴 ·s 𝐵))) | 
| 146 | 144, 145 | sylbi 217 | . . . 4
⊢ (𝑦 ∈ {(𝐴 ·s 𝐵)} → (𝑥 <s 𝑦 ↔ 𝑥 <s (𝐴 ·s 𝐵))) | 
| 147 | 143, 146 | syl5ibrcom 247 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) → (𝑦 ∈ {(𝐴 ·s 𝐵)} → 𝑥 <s 𝑦)) | 
| 148 | 147 | 3impia 1117 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ∧ 𝑦 ∈ {(𝐴 ·s 𝐵)}) → 𝑥 <s 𝑦) | 
| 149 | 25, 27, 76, 78, 148 | ssltd 27837 | 1
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)}) |