Step | Hyp | Ref
| Expression |
1 | | mulscut.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | mulscut.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | 1, 2 | mulscutlem 27516 |
. 2
⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No
∧ ({𝑓 ∣
∃𝑔 ∈ ( L
‘𝐴)∃ℎ ∈ ( L ‘𝐵)𝑓 = (((𝑔 ·s 𝐵) +s (𝐴 ·s ℎ)) -s (𝑔 ·s ℎ))} ∪ {𝑖 ∣ ∃𝑗 ∈ ( R ‘𝐴)∃𝑘 ∈ ( R ‘𝐵)𝑖 = (((𝑗 ·s 𝐵) +s (𝐴 ·s 𝑘)) -s (𝑗 ·s 𝑘))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑙 ∣ ∃𝑚 ∈ ( L ‘𝐴)∃𝑛 ∈ ( R ‘𝐵)𝑙 = (((𝑚 ·s 𝐵) +s (𝐴 ·s 𝑛)) -s (𝑚 ·s 𝑛))} ∪ {𝑜 ∣ ∃𝑥 ∈ ( R ‘𝐴)∃𝑦 ∈ ( L ‘𝐵)𝑜 = (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦))}))) |
4 | | biid 260 |
. . 3
⊢ ((𝐴 ·s 𝐵) ∈
No ↔ (𝐴
·s 𝐵)
∈ No ) |
5 | | mulsval2lem 27495 |
. . . . 5
⊢ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} = {𝑓 ∣ ∃𝑔 ∈ ( L ‘𝐴)∃ℎ ∈ ( L ‘𝐵)𝑓 = (((𝑔 ·s 𝐵) +s (𝐴 ·s ℎ)) -s (𝑔 ·s ℎ))} |
6 | | mulsval2lem 27495 |
. . . . 5
⊢ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} = {𝑖 ∣ ∃𝑗 ∈ ( R ‘𝐴)∃𝑘 ∈ ( R ‘𝐵)𝑖 = (((𝑗 ·s 𝐵) +s (𝐴 ·s 𝑘)) -s (𝑗 ·s 𝑘))} |
7 | 5, 6 | uneq12i 4158 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ({𝑓 ∣ ∃𝑔 ∈ ( L ‘𝐴)∃ℎ ∈ ( L ‘𝐵)𝑓 = (((𝑔 ·s 𝐵) +s (𝐴 ·s ℎ)) -s (𝑔 ·s ℎ))} ∪ {𝑖 ∣ ∃𝑗 ∈ ( R ‘𝐴)∃𝑘 ∈ ( R ‘𝐵)𝑖 = (((𝑗 ·s 𝐵) +s (𝐴 ·s 𝑘)) -s (𝑗 ·s 𝑘))}) |
8 | 7 | breq1i 5149 |
. . 3
⊢ (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ↔ ({𝑓 ∣ ∃𝑔 ∈ ( L ‘𝐴)∃ℎ ∈ ( L ‘𝐵)𝑓 = (((𝑔 ·s 𝐵) +s (𝐴 ·s ℎ)) -s (𝑔 ·s ℎ))} ∪ {𝑖 ∣ ∃𝑗 ∈ ( R ‘𝐴)∃𝑘 ∈ ( R ‘𝐵)𝑖 = (((𝑗 ·s 𝐵) +s (𝐴 ·s 𝑘)) -s (𝑗 ·s 𝑘))}) <<s {(𝐴 ·s 𝐵)}) |
9 | | mulsval2lem 27495 |
. . . . 5
⊢ {𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} = {𝑙 ∣ ∃𝑚 ∈ ( L ‘𝐴)∃𝑛 ∈ ( R ‘𝐵)𝑙 = (((𝑚 ·s 𝐵) +s (𝐴 ·s 𝑛)) -s (𝑚 ·s 𝑛))} |
10 | | mulsval2lem 27495 |
. . . . 5
⊢ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))} = {𝑜 ∣ ∃𝑥 ∈ ( R ‘𝐴)∃𝑦 ∈ ( L ‘𝐵)𝑜 = (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦))} |
11 | 9, 10 | uneq12i 4158 |
. . . 4
⊢ ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ({𝑙 ∣ ∃𝑚 ∈ ( L ‘𝐴)∃𝑛 ∈ ( R ‘𝐵)𝑙 = (((𝑚 ·s 𝐵) +s (𝐴 ·s 𝑛)) -s (𝑚 ·s 𝑛))} ∪ {𝑜 ∣ ∃𝑥 ∈ ( R ‘𝐴)∃𝑦 ∈ ( L ‘𝐵)𝑜 = (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦))}) |
12 | 11 | breq2i 5150 |
. . 3
⊢ ({(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) ↔ {(𝐴 ·s 𝐵)} <<s ({𝑙 ∣ ∃𝑚 ∈ ( L ‘𝐴)∃𝑛 ∈ ( R ‘𝐵)𝑙 = (((𝑚 ·s 𝐵) +s (𝐴 ·s 𝑛)) -s (𝑚 ·s 𝑛))} ∪ {𝑜 ∣ ∃𝑥 ∈ ( R ‘𝐴)∃𝑦 ∈ ( L ‘𝐵)𝑜 = (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦))})) |
13 | 4, 8, 12 | 3anbi123i 1155 |
. 2
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ ({𝑎
∣ ∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) ↔ ((𝐴 ·s 𝐵) ∈ No
∧ ({𝑓 ∣
∃𝑔 ∈ ( L
‘𝐴)∃ℎ ∈ ( L ‘𝐵)𝑓 = (((𝑔 ·s 𝐵) +s (𝐴 ·s ℎ)) -s (𝑔 ·s ℎ))} ∪ {𝑖 ∣ ∃𝑗 ∈ ( R ‘𝐴)∃𝑘 ∈ ( R ‘𝐵)𝑖 = (((𝑗 ·s 𝐵) +s (𝐴 ·s 𝑘)) -s (𝑗 ·s 𝑘))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑙 ∣ ∃𝑚 ∈ ( L ‘𝐴)∃𝑛 ∈ ( R ‘𝐵)𝑙 = (((𝑚 ·s 𝐵) +s (𝐴 ·s 𝑛)) -s (𝑚 ·s 𝑛))} ∪ {𝑜 ∣ ∃𝑥 ∈ ( R ‘𝐴)∃𝑦 ∈ ( L ‘𝐵)𝑜 = (((𝑥 ·s 𝐵) +s (𝐴 ·s 𝑦)) -s (𝑥 ·s 𝑦))}))) |
14 | 3, 13 | sylibr 233 |
1
⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No
∧ ({𝑎 ∣
∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |