Step | Hyp | Ref
| Expression |
1 | | isthincd2lem2.6 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
2 | | oveq1 7241 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑦) = (𝑤𝐻𝑦)) |
3 | | opeq1 4800 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → 〈𝑥, 𝑦〉 = 〈𝑤, 𝑦〉) |
4 | 3 | oveq1d 7249 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑤, 𝑦〉 · 𝑧)) |
5 | 4 | oveqd 7251 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓)) |
6 | | oveq1 7241 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥𝐻𝑧) = (𝑤𝐻𝑧)) |
7 | 5, 6 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
8 | 7 | ralbidv 3120 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
9 | 2, 8 | raleqbidv 3327 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
10 | | oveq2 7242 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (𝑤𝐻𝑦) = (𝑤𝐻𝑣)) |
11 | | oveq1 7241 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (𝑦𝐻𝑧) = (𝑣𝐻𝑧)) |
12 | | opeq2 4801 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 〈𝑤, 𝑦〉 = 〈𝑤, 𝑣〉) |
13 | 12 | oveq1d 7249 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (〈𝑤, 𝑦〉 · 𝑧) = (〈𝑤, 𝑣〉 · 𝑧)) |
14 | 13 | oveqd 7251 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓)) |
15 | 14 | eleq1d 2824 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → ((𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
16 | 11, 15 | raleqbidv 3327 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
17 | 10, 16 | raleqbidv 3327 |
. . . . 5
⊢ (𝑦 = 𝑣 → (∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑤, 𝑦〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧))) |
18 | | oveq2 7242 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → (𝑣𝐻𝑧) = (𝑣𝐻𝑢)) |
19 | | oveq2 7242 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (〈𝑤, 𝑣〉 · 𝑧) = (〈𝑤, 𝑣〉 · 𝑢)) |
20 | 19 | oveqd 7251 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) = (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓)) |
21 | | oveq2 7242 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (𝑤𝐻𝑧) = (𝑤𝐻𝑢)) |
22 | 20, 21 | eleq12d 2834 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → ((𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) ∈ (𝑤𝐻𝑢))) |
23 | 18, 22 | raleqbidv 3327 |
. . . . . . 7
⊢ (𝑧 = 𝑢 → (∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) ∈ (𝑤𝐻𝑢))) |
24 | 23 | ralbidv 3120 |
. . . . . 6
⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) ∈ (𝑤𝐻𝑢))) |
25 | | oveq2 7242 |
. . . . . . . 8
⊢ (𝑓 = 𝑘 → (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) = (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑘)) |
26 | 25 | eleq1d 2824 |
. . . . . . 7
⊢ (𝑓 = 𝑘 → ((𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))) |
27 | | oveq1 7241 |
. . . . . . . 8
⊢ (𝑔 = 𝑙 → (𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑘) = (𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘)) |
28 | 27 | eleq1d 2824 |
. . . . . . 7
⊢ (𝑔 = 𝑙 → ((𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))) |
29 | 26, 28 | cbvral2vw 3385 |
. . . . . 6
⊢
(∀𝑓 ∈
(𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(〈𝑤, 𝑣〉 · 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)) |
30 | 24, 29 | bitrdi 290 |
. . . . 5
⊢ (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(〈𝑤, 𝑣〉 · 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢))) |
31 | 9, 17, 30 | cbvral3vw 3387 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)) |
32 | 1, 31 | sylib 221 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢)) |
33 | | isthincd2lem2.1 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
34 | | isthincd2lem2.2 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
35 | | isthincd2lem2.3 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
36 | | oveq1 7241 |
. . . . . 6
⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑣) = (𝑋𝐻𝑣)) |
37 | | opeq1 4800 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑋 → 〈𝑤, 𝑣〉 = 〈𝑋, 𝑣〉) |
38 | 37 | oveq1d 7249 |
. . . . . . . . 9
⊢ (𝑤 = 𝑋 → (〈𝑤, 𝑣〉 · 𝑢) = (〈𝑋, 𝑣〉 · 𝑢)) |
39 | 38 | oveqd 7251 |
. . . . . . . 8
⊢ (𝑤 = 𝑋 → (𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) = (𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘)) |
40 | | oveq1 7241 |
. . . . . . . 8
⊢ (𝑤 = 𝑋 → (𝑤𝐻𝑢) = (𝑋𝐻𝑢)) |
41 | 39, 40 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑤 = 𝑋 → ((𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
42 | 41 | ralbidv 3120 |
. . . . . 6
⊢ (𝑤 = 𝑋 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
43 | 36, 42 | raleqbidv 3327 |
. . . . 5
⊢ (𝑤 = 𝑋 → (∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
44 | | oveq2 7242 |
. . . . . 6
⊢ (𝑣 = 𝑌 → (𝑋𝐻𝑣) = (𝑋𝐻𝑌)) |
45 | | oveq1 7241 |
. . . . . . 7
⊢ (𝑣 = 𝑌 → (𝑣𝐻𝑢) = (𝑌𝐻𝑢)) |
46 | | opeq2 4801 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑌 → 〈𝑋, 𝑣〉 = 〈𝑋, 𝑌〉) |
47 | 46 | oveq1d 7249 |
. . . . . . . . 9
⊢ (𝑣 = 𝑌 → (〈𝑋, 𝑣〉 · 𝑢) = (〈𝑋, 𝑌〉 · 𝑢)) |
48 | 47 | oveqd 7251 |
. . . . . . . 8
⊢ (𝑣 = 𝑌 → (𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) = (𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘)) |
49 | 48 | eleq1d 2824 |
. . . . . . 7
⊢ (𝑣 = 𝑌 → ((𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
50 | 45, 49 | raleqbidv 3327 |
. . . . . 6
⊢ (𝑣 = 𝑌 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
51 | 44, 50 | raleqbidv 3327 |
. . . . 5
⊢ (𝑣 = 𝑌 → (∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑋, 𝑣〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢))) |
52 | | oveq2 7242 |
. . . . . . 7
⊢ (𝑢 = 𝑍 → (𝑌𝐻𝑢) = (𝑌𝐻𝑍)) |
53 | | oveq2 7242 |
. . . . . . . . 9
⊢ (𝑢 = 𝑍 → (〈𝑋, 𝑌〉 · 𝑢) = (〈𝑋, 𝑌〉 · 𝑍)) |
54 | 53 | oveqd 7251 |
. . . . . . . 8
⊢ (𝑢 = 𝑍 → (𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) = (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘)) |
55 | | oveq2 7242 |
. . . . . . . 8
⊢ (𝑢 = 𝑍 → (𝑋𝐻𝑢) = (𝑋𝐻𝑍)) |
56 | 54, 55 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑢 = 𝑍 → ((𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))) |
57 | 52, 56 | raleqbidv 3327 |
. . . . . 6
⊢ (𝑢 = 𝑍 → (∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))) |
58 | 57 | ralbidv 3120 |
. . . . 5
⊢ (𝑢 = 𝑍 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(〈𝑋, 𝑌〉 · 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))) |
59 | 43, 51, 58 | rspc3v 3564 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))) |
60 | 33, 34, 35, 59 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (∀𝑤 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(〈𝑤, 𝑣〉 · 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍))) |
61 | 32, 60 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍)) |
62 | | isthincd2lem2.4 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
63 | | isthincd2lem2.5 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) |
64 | | oveq2 7242 |
. . . . 5
⊢ (𝑘 = 𝐹 → (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) = (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝐹)) |
65 | 64 | eleq1d 2824 |
. . . 4
⊢ (𝑘 = 𝐹 → ((𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) ↔ (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))) |
66 | | oveq1 7241 |
. . . . 5
⊢ (𝑙 = 𝐺 → (𝑙(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) |
67 | 66 | eleq1d 2824 |
. . . 4
⊢ (𝑙 = 𝐺 → ((𝑙(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍) ↔ (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))) |
68 | 65, 67 | rspc2v 3561 |
. . 3
⊢ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑍)) → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))) |
69 | 62, 63, 68 | syl2anc 587 |
. 2
⊢ (𝜑 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(〈𝑋, 𝑌〉 · 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))) |
70 | 61, 69 | mpd 15 |
1
⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) |