Proof of Theorem mulscut2
Step | Hyp | Ref
| Expression |
1 | | mulscut.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | mulscut.2 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | 1, 2 | mulscut 27568 |
. . . 4
⊢ (𝜑 → ((𝐴 ·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 | | 3anass 1096 |
. . . 4
⊢ (((𝐴 ·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 𝑤))})))) |
5 | 3, 4 | sylib 217 |
. . 3
⊢ (𝜑 → ((𝐴 ·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 𝑤))})))) |
6 | 5 | simprd 497 |
. 2
⊢ (𝜑 → (({𝑎 ∣ ∃𝑝 ∈ ( 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 𝑤))}))) |
7 | | ovex 7437 |
. . . 4
⊢ (𝐴 ·s 𝐵) ∈ V |
8 | 7 | snnz 4779 |
. . 3
⊢ {(𝐴 ·s 𝐵)} ≠ ∅ |
9 | | sslttr 27288 |
. . 3
⊢ ((({𝑎 ∣ ∃𝑝 ∈ ( 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 𝐵)} ≠ ∅) → ({𝑎 ∣ ∃𝑝 ∈ ( 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 𝑤))})) |
10 | 8, 9 | mp3an3 1451 |
. 2
⊢ ((({𝑎 ∣ ∃𝑝 ∈ ( 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 𝑤))})) → ({𝑎 ∣ ∃𝑝 ∈ ( 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 𝑤))})) |
11 | 6, 10 | syl 17 |
1
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ ( 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 𝑤))})) |