Proof of Theorem eroprf
Step | Hyp | Ref
| Expression |
1 | | eropr.3 |
. . . . . . . . . . . 12
⊢ (φ → 𝑇 ∈ 𝑍) |
2 | 1 | ad2antrr 457 |
. . . . . . . . . . 11
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ 𝑇 ∈ 𝑍) |
3 | | eropr.10 |
. . . . . . . . . . . . 13
⊢ (φ → + :(A × B)⟶𝐶) |
4 | 3 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → + :(A × B)⟶𝐶) |
5 | 4 | fovrnda 5586 |
. . . . . . . . . . 11
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ (𝑝 + 𝑞) ∈ 𝐶) |
6 | | ecelqsg 6095 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑍 ∧ (𝑝 + 𝑞) ∈ 𝐶) → [(𝑝 + 𝑞)]𝑇 ∈ (𝐶 / 𝑇)) |
7 | 2, 5, 6 | syl2anc 391 |
. . . . . . . . . 10
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ [(𝑝 + 𝑞)]𝑇 ∈ (𝐶 / 𝑇)) |
8 | | eropr.15 |
. . . . . . . . . 10
⊢ 𝐿 = (𝐶 / 𝑇) |
9 | 7, 8 | syl6eleqr 2128 |
. . . . . . . . 9
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ [(𝑝 + 𝑞)]𝑇 ∈ 𝐿) |
10 | | eleq1a 2106 |
. . . . . . . . 9
⊢ ([(𝑝 + 𝑞)]𝑇 ∈ 𝐿 → (z = [(𝑝 + 𝑞)]𝑇 → z ∈ 𝐿)) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ (z = [(𝑝 + 𝑞)]𝑇 → z ∈ 𝐿)) |
12 | 11 | adantld 263 |
. . . . . . 7
⊢ (((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) ∧ (𝑝 ∈ A ∧ 𝑞
∈ B))
→ (((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → z ∈ 𝐿)) |
13 | 12 | rexlimdvva 2434 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → z ∈ 𝐿)) |
14 | 13 | abssdv 3008 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → {z ∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)} ⊆ 𝐿) |
15 | | eropr.1 |
. . . . . . 7
⊢ 𝐽 = (A / 𝑅) |
16 | | eropr.2 |
. . . . . . 7
⊢ 𝐾 = (B / 𝑆) |
17 | | eropr.4 |
. . . . . . 7
⊢ (φ → 𝑅 Er 𝑈) |
18 | | eropr.5 |
. . . . . . 7
⊢ (φ → 𝑆 Er 𝑉) |
19 | | eropr.6 |
. . . . . . 7
⊢ (φ → 𝑇 Er 𝑊) |
20 | | eropr.7 |
. . . . . . 7
⊢ (φ → A ⊆ 𝑈) |
21 | | eropr.8 |
. . . . . . 7
⊢ (φ → B ⊆ 𝑉) |
22 | | eropr.9 |
. . . . . . 7
⊢ (φ → 𝐶 ⊆ 𝑊) |
23 | | eropr.11 |
. . . . . . 7
⊢ ((φ ∧ ((𝑟 ∈ A ∧ 𝑠
∈ A)
∧ (𝑡 ∈ B ∧ u ∈ B))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆u)
→ (𝑟 + 𝑡)𝑇(𝑠 + u))) |
24 | 15, 16, 1, 17, 18, 19, 20, 21, 22, 3, 23 | eroveu 6133 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → ∃!z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) |
25 | | iotacl 4833 |
. . . . . 6
⊢ (∃!z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ∈
{z ∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)}) |
26 | 24, 25 | syl 14 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ∈
{z ∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)}) |
27 | 14, 26 | sseldd 2940 |
. . . 4
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ∈ 𝐿) |
28 | 27 | ralrimivva 2395 |
. . 3
⊢ (φ → ∀x ∈ 𝐽 ∀y ∈ 𝐾 (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ∈ 𝐿) |
29 | | eqid 2037 |
. . . 4
⊢ (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) = (x
∈ 𝐽, y
∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) |
30 | 29 | fmpt2 5769 |
. . 3
⊢ (∀x ∈ 𝐽 ∀y ∈ 𝐾 (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ∈ 𝐿 ↔ (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))):(𝐽 × 𝐾)⟶𝐿) |
31 | 28, 30 | sylib 127 |
. 2
⊢ (φ → (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))):(𝐽 × 𝐾)⟶𝐿) |
32 | | eropr.12 |
. . . 4
⊢ ⨣ =
{〈〈x, y〉, z〉
∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)} |
33 | 15, 16, 1, 17, 18, 19, 20, 21, 22, 3, 23, 32 | erovlem 6134 |
. . 3
⊢ (φ → ⨣ = (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))) |
34 | 33 | feq1d 4977 |
. 2
⊢ (φ → ( ⨣ :(𝐽 × 𝐾)⟶𝐿 ↔ (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))):(𝐽 × 𝐾)⟶𝐿)) |
35 | 31, 34 | mpbird 156 |
1
⊢ (φ → ⨣ :(𝐽 × 𝐾)⟶𝐿) |