Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
⊢ (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) = (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
2 | 1 | rnmpo 7537 |
. . . 4
⊢ ran
(𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) = {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} |
3 | | ssltmul1.1 |
. . . . . . 7
⊢ (𝜑 → 𝐿 <<s 𝑅) |
4 | | ssltex1 27268 |
. . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ V) |
6 | | ssltmul1.2 |
. . . . . . 7
⊢ (𝜑 → 𝑀 <<s 𝑆) |
7 | | ssltex1 27268 |
. . . . . . 7
⊢ (𝑀 <<s 𝑆 → 𝑀 ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ V) |
9 | 1 | mpoexg 8058 |
. . . . . 6
⊢ ((𝐿 ∈ V ∧ 𝑀 ∈ V) → (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) |
10 | 5, 8, 9 | syl2anc 585 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ 𝐿, 𝑞 ∈ 𝑀 ↦ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) ∈ V) |
11 | | rnexg 7890 |
. . . . 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 2839 |
. . 3
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∈ V) |
14 | | eqid 2733 |
. . . . 5
⊢ (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) = (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
15 | 14 | rnmpo 7537 |
. . . 4
⊢ ran
(𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) = {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} |
16 | | ssltex2 27269 |
. . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) |
17 | 3, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ V) |
18 | | ssltex2 27269 |
. . . . . . 7
⊢ (𝑀 <<s 𝑆 → 𝑆 ∈ V) |
19 | 6, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
20 | 14 | mpoexg 8058 |
. . . . . 6
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) |
21 | 17, 19, 20 | syl2anc 585 |
. . . . 5
⊢ (𝜑 → (𝑟 ∈ 𝑅, 𝑠 ∈ 𝑆 ↦ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) ∈ V) |
22 | | rnexg 7890 |
. . . . 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 2839 |
. . 3
⊢ (𝜑 → {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ∈ V) |
25 | 13, 24 | unexd 7736 |
. 2
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ∈ V) |
26 | | snex 5430 |
. . 3
⊢ {(𝐴 ·s 𝐵)} ∈ V |
27 | 26 | a1i 11 |
. 2
⊢ (𝜑 → {(𝐴 ·s 𝐵)} ∈ V) |
28 | | ssltss1 27270 |
. . . . . . . . . . . 12
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No
) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ⊆ No
) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐿 ⊆ No
) |
31 | | simprl 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 ∈ 𝐿) |
32 | 30, 31 | sseldd 3982 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 ∈ No
) |
33 | | ssltmul1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆)) |
34 | 6 | scutcld 27284 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 |s 𝑆) ∈ No
) |
35 | 33, 34 | eqeltrd 2834 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ No
) |
36 | 35 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐵 ∈ No
) |
37 | 32, 36 | mulscld 27571 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝐵) ∈ No
) |
38 | | ssltmul1.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) |
39 | 3 | scutcld 27284 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No
) |
40 | 38, 39 | eqeltrd 2834 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ No
) |
41 | 40 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐴 ∈ No
) |
42 | | ssltss1 27270 |
. . . . . . . . . . . 12
⊢ (𝑀 <<s 𝑆 → 𝑀 ⊆ No
) |
43 | 6, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ⊆ No
) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑀 ⊆ No
) |
45 | | simprr 772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 ∈ 𝑀) |
46 | 44, 45 | sseldd 3982 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 ∈ No
) |
47 | 41, 46 | mulscld 27571 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝑞) ∈ No
) |
48 | 37, 47 | addscld 27444 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) ∈ No
) |
49 | 32, 46 | mulscld 27571 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑝 ·s 𝑞) ∈ No
) |
50 | 48, 49 | subscld 27515 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∈ No
) |
51 | | eleq1 2822 |
. . . . . 6
⊢ (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → (𝑎 ∈ No
↔ (((𝑝
·s 𝐵)
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))
∈ No )) |
52 | 50, 51 | syl5ibrcom 246 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑎 ∈ No
)) |
53 | 52 | rexlimdvva 3212 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → 𝑎 ∈ No
)) |
54 | 53 | abssdv 4064 |
. . 3
⊢ (𝜑 → {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ⊆ No
) |
55 | | ssltss2 27271 |
. . . . . . . . . . . 12
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No
) |
56 | 3, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ⊆ No
) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑅 ⊆ No
) |
58 | | simprl 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑟 ∈ 𝑅) |
59 | 57, 58 | sseldd 3982 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑟 ∈ No
) |
60 | 35 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 ∈ No
) |
61 | 59, 60 | mulscld 27571 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝐵) ∈ No
) |
62 | 40 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 ∈ No
) |
63 | | ssltss2 27271 |
. . . . . . . . . . . 12
⊢ (𝑀 <<s 𝑆 → 𝑆 ⊆ No
) |
64 | 6, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ No
) |
65 | 64 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑆 ⊆ No
) |
66 | | simprr 772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑠 ∈ 𝑆) |
67 | 65, 66 | sseldd 3982 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑠 ∈ No
) |
68 | 62, 67 | mulscld 27571 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝑠) ∈ No
) |
69 | 61, 68 | addscld 27444 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) ∈ No
) |
70 | 59, 67 | mulscld 27571 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 ·s 𝑠) ∈ No
) |
71 | 69, 70 | subscld 27515 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ∈ No
) |
72 | | eleq1 2822 |
. . . . . 6
⊢ (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → (𝑏 ∈ No
↔ (((𝑟
·s 𝐵)
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠))
∈ No )) |
73 | 71, 72 | syl5ibrcom 246 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑏 ∈ No
)) |
74 | 73 | rexlimdvva 3212 |
. . . 4
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑏 ∈ No
)) |
75 | 74 | abssdv 4064 |
. . 3
⊢ (𝜑 → {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))} ⊆ No
) |
76 | 54, 75 | unssd 4185 |
. 2
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ⊆ No
) |
77 | 40, 35 | mulscld 27571 |
. . 3
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ No
) |
78 | 77 | snssd 4811 |
. 2
⊢ (𝜑 → {(𝐴 ·s 𝐵)} ⊆ No
) |
79 | | elun 4147 |
. . . . . . 7
⊢ (𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ↔ (𝑥 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∨ 𝑥 ∈ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) |
80 | | vex 3479 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
81 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) |
82 | 81 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)))) |
83 | 80, 82 | elab 3667 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ↔ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
84 | | eqeq1 2737 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑥 → (𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) |
85 | 84 | 2rexbidv 3220 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)))) |
86 | 80, 85 | elab 3667 |
. . . . . . . 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 27529 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) +s (𝐴 ·s 𝑞))) |
90 | | scutcut 27282 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
91 | 3, 90 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
92 | 91 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 <<s {(𝐿 |s 𝑅)}) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐿 <<s {(𝐿 |s 𝑅)}) |
94 | | ovex 7437 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 |s 𝑅) ∈ V |
95 | 94 | snid 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 |s 𝑅) ∈ {(𝐿 |s 𝑅)} |
96 | 38, 95 | eqeltrdi 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ {(𝐿 |s 𝑅)}) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐴 ∈ {(𝐿 |s 𝑅)}) |
98 | 93, 31, 97 | ssltsepcd 27275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑝 <s 𝐴) |
99 | | scutcut 27282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 <<s 𝑆 → ((𝑀 |s 𝑆) ∈ No
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) |
100 | 6, 99 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 |s 𝑆) ∈ No
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) |
101 | 100 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 <<s {(𝑀 |s 𝑆)}) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑀 <<s {(𝑀 |s 𝑆)}) |
103 | | ovex 7437 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 |s 𝑆) ∈ V |
104 | 103 | snid 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 |s 𝑆) ∈ {(𝑀 |s 𝑆)} |
105 | 33, 104 | eqeltrdi 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ {(𝑀 |s 𝑆)}) |
106 | 105 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝐵 ∈ {(𝑀 |s 𝑆)}) |
107 | 102, 45, 106 | ssltsepcd 27275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → 𝑞 <s 𝐵) |
108 | 32, 41, 46, 36, 98, 107 | sltmuld 27573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑞))) |
109 | 37, 49 | subscld 27515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → ((𝑝 ·s 𝐵) -s (𝑝 ·s 𝑞)) ∈ No
) |
110 | 77 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (𝐴 ·s 𝐵) ∈ No
) |
111 | 109, 47, 110 | sltaddsubd 27538 |
. . . . . . . . . . 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 5169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀)) → (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) <s (𝐴 ·s 𝐵)) |
114 | | breq1 5150 |
. . . . . . . . 9
⊢ (𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) → (𝑥 <s (𝐴 ·s 𝐵) ↔ (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) <s (𝐴 ·s 𝐵))) |
115 | 113, 114 | syl5ibrcom 246 |
. . . . . . . 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 27529 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) = (((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠))) |
118 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐿 <<s 𝑅) |
119 | 118, 90 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
120 | 119 | simp3d 1145 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {(𝐿 |s 𝑅)} <<s 𝑅) |
121 | 38 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 = (𝐿 |s 𝑅)) |
122 | 121, 95 | eqeltrdi 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 ∈ {(𝐿 |s 𝑅)}) |
123 | 120, 122,
58 | ssltsepcd 27275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐴 <s 𝑟) |
124 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝑀 <<s 𝑆) |
125 | 124, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑀 |s 𝑆) ∈ No
∧ 𝑀 <<s {(𝑀 |s 𝑆)} ∧ {(𝑀 |s 𝑆)} <<s 𝑆)) |
126 | 125 | simp3d 1145 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → {(𝑀 |s 𝑆)} <<s 𝑆) |
127 | 33 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 = (𝑀 |s 𝑆)) |
128 | 127, 104 | eqeltrdi 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 ∈ {(𝑀 |s 𝑆)}) |
129 | 126, 128,
66 | ssltsepcd 27275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → 𝐵 <s 𝑠) |
130 | 62, 59, 60, 67, 123, 129 | sltmuld 27573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝐴 ·s 𝑠) -s (𝐴 ·s 𝐵)) <s ((𝑟 ·s 𝑠) -s (𝑟 ·s 𝐵))) |
131 | 61, 70 | subscld 27515 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) ∈ No
) |
132 | 77 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝐴 ·s 𝐵) ∈ No
) |
133 | 131, 68, 132 | sltaddsubd 27538 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) +s (𝐴 ·s 𝑠)) <s (𝐴 ·s 𝐵) ↔ ((𝑟 ·s 𝐵) -s (𝑟 ·s 𝑠)) <s ((𝐴 ·s 𝐵) -s (𝐴 ·s 𝑠)))) |
134 | 61, 70, 132, 68 | sltsubsub2bd 27531 |
. . . . . . . . . . . 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 5169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) <s (𝐴 ·s 𝐵)) |
138 | | breq1 5150 |
. . . . . . . . 9
⊢ (𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → (𝑥 <s (𝐴 ·s 𝐵) ↔ (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) <s (𝐴 ·s 𝐵))) |
139 | 137, 138 | syl5ibrcom 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑥 <s (𝐴 ·s 𝐵))) |
140 | 139 | rexlimdvva 3212 |
. . . . . . 7
⊢ (𝜑 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) → 𝑥 <s (𝐴 ·s 𝐵))) |
141 | 116, 140 | jaod 858 |
. . . . . 6
⊢ (𝜑 → ((∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑥 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ∨ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑥 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) → 𝑥 <s (𝐴 ·s 𝐵))) |
142 | 88, 141 | biimtrid 241 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) → 𝑥 <s (𝐴 ·s 𝐵))) |
143 | 142 | imp 408 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) → 𝑥 <s (𝐴 ·s 𝐵)) |
144 | | velsn 4643 |
. . . . 5
⊢ (𝑦 ∈ {(𝐴 ·s 𝐵)} ↔ 𝑦 = (𝐴 ·s 𝐵)) |
145 | | breq2 5151 |
. . . . 5
⊢ (𝑦 = (𝐴 ·s 𝐵) → (𝑥 <s 𝑦 ↔ 𝑥 <s (𝐴 ·s 𝐵))) |
146 | 144, 145 | sylbi 216 |
. . . 4
⊢ (𝑦 ∈ {(𝐴 ·s 𝐵)} → (𝑥 <s 𝑦 ↔ 𝑥 <s (𝐴 ·s 𝐵))) |
147 | 143, 146 | syl5ibrcom 246 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))})) → (𝑦 ∈ {(𝐴 ·s 𝐵)} → 𝑥 <s 𝑦)) |
148 | 147 | 3impia 1118 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) ∧ 𝑦 ∈ {(𝐴 ·s 𝐵)}) → 𝑥 <s 𝑦) |
149 | 25, 27, 76, 78, 148 | ssltd 27273 |
1
⊢ (𝜑 → ({𝑎 ∣ ∃𝑝 ∈ 𝐿 ∃𝑞 ∈ 𝑀 𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)}) |