Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isthincd2lem2 Structured version   Visualization version   GIF version

Theorem isthincd2lem2 46023
Description: Lemma for isthincd2 46025. (Contributed by Zhi Wang, 17-Sep-2024.)
Hypotheses
Ref Expression
isthincd2lem2.1 (𝜑𝑋𝐵)
isthincd2lem2.2 (𝜑𝑌𝐵)
isthincd2lem2.3 (𝜑𝑍𝐵)
isthincd2lem2.4 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
isthincd2lem2.5 (𝜑𝐺 ∈ (𝑌𝐻𝑍))
isthincd2lem2.6 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
Assertion
Ref Expression
isthincd2lem2 (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Distinct variable groups:   · ,𝑓,𝑔,𝑧,𝑥,𝑦   𝑧,𝐵,𝑥,𝑦   𝑓,𝐻,𝑔,𝑧,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐵(𝑓,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑋(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑍(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem isthincd2lem2
Dummy variables 𝑘 𝑢 𝑣 𝑤 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isthincd2lem2.6 . . . 4 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧))
2 oveq1 7241 . . . . . 6 (𝑥 = 𝑤 → (𝑥𝐻𝑦) = (𝑤𝐻𝑦))
3 opeq1 4800 . . . . . . . . . 10 (𝑥 = 𝑤 → ⟨𝑥, 𝑦⟩ = ⟨𝑤, 𝑦⟩)
43oveq1d 7249 . . . . . . . . 9 (𝑥 = 𝑤 → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑤, 𝑦· 𝑧))
54oveqd 7251 . . . . . . . 8 (𝑥 = 𝑤 → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑦· 𝑧)𝑓))
6 oveq1 7241 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥𝐻𝑧) = (𝑤𝐻𝑧))
75, 6eleq12d 2834 . . . . . . 7 (𝑥 = 𝑤 → ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
87ralbidv 3120 . . . . . 6 (𝑥 = 𝑤 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
92, 8raleqbidv 3327 . . . . 5 (𝑥 = 𝑤 → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
10 oveq2 7242 . . . . . 6 (𝑦 = 𝑣 → (𝑤𝐻𝑦) = (𝑤𝐻𝑣))
11 oveq1 7241 . . . . . . 7 (𝑦 = 𝑣 → (𝑦𝐻𝑧) = (𝑣𝐻𝑧))
12 opeq2 4801 . . . . . . . . . 10 (𝑦 = 𝑣 → ⟨𝑤, 𝑦⟩ = ⟨𝑤, 𝑣⟩)
1312oveq1d 7249 . . . . . . . . 9 (𝑦 = 𝑣 → (⟨𝑤, 𝑦· 𝑧) = (⟨𝑤, 𝑣· 𝑧))
1413oveqd 7251 . . . . . . . 8 (𝑦 = 𝑣 → (𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣· 𝑧)𝑓))
1514eleq1d 2824 . . . . . . 7 (𝑦 = 𝑣 → ((𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
1611, 15raleqbidv 3327 . . . . . 6 (𝑦 = 𝑣 → (∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
1710, 16raleqbidv 3327 . . . . 5 (𝑦 = 𝑣 → (∀𝑓 ∈ (𝑤𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑤, 𝑦· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧)))
18 oveq2 7242 . . . . . . . 8 (𝑧 = 𝑢 → (𝑣𝐻𝑧) = (𝑣𝐻𝑢))
19 oveq2 7242 . . . . . . . . . 10 (𝑧 = 𝑢 → (⟨𝑤, 𝑣· 𝑧) = (⟨𝑤, 𝑣· 𝑢))
2019oveqd 7251 . . . . . . . . 9 (𝑧 = 𝑢 → (𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) = (𝑔(⟨𝑤, 𝑣· 𝑢)𝑓))
21 oveq2 7242 . . . . . . . . 9 (𝑧 = 𝑢 → (𝑤𝐻𝑧) = (𝑤𝐻𝑢))
2220, 21eleq12d 2834 . . . . . . . 8 (𝑧 = 𝑢 → ((𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ (𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
2318, 22raleqbidv 3327 . . . . . . 7 (𝑧 = 𝑢 → (∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
2423ralbidv 3120 . . . . . 6 (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) ∈ (𝑤𝐻𝑢)))
25 oveq2 7242 . . . . . . . 8 (𝑓 = 𝑘 → (𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) = (𝑔(⟨𝑤, 𝑣· 𝑢)𝑘))
2625eleq1d 2824 . . . . . . 7 (𝑓 = 𝑘 → ((𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ (𝑔(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
27 oveq1 7241 . . . . . . . 8 (𝑔 = 𝑙 → (𝑔(⟨𝑤, 𝑣· 𝑢)𝑘) = (𝑙(⟨𝑤, 𝑣· 𝑢)𝑘))
2827eleq1d 2824 . . . . . . 7 (𝑔 = 𝑙 → ((𝑔(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
2926, 28cbvral2vw 3385 . . . . . 6 (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑢)(𝑔(⟨𝑤, 𝑣· 𝑢)𝑓) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
3024, 29bitrdi 290 . . . . 5 (𝑧 = 𝑢 → (∀𝑓 ∈ (𝑤𝐻𝑣)∀𝑔 ∈ (𝑣𝐻𝑧)(𝑔(⟨𝑤, 𝑣· 𝑧)𝑓) ∈ (𝑤𝐻𝑧) ↔ ∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢)))
319, 17, 30cbvral3vw 3387 . . . 4 (∀𝑥𝐵𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ ∀𝑤𝐵𝑣𝐵𝑢𝐵𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
321, 31sylib 221 . . 3 (𝜑 → ∀𝑤𝐵𝑣𝐵𝑢𝐵𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢))
33 isthincd2lem2.1 . . . 4 (𝜑𝑋𝐵)
34 isthincd2lem2.2 . . . 4 (𝜑𝑌𝐵)
35 isthincd2lem2.3 . . . 4 (𝜑𝑍𝐵)
36 oveq1 7241 . . . . . 6 (𝑤 = 𝑋 → (𝑤𝐻𝑣) = (𝑋𝐻𝑣))
37 opeq1 4800 . . . . . . . . . 10 (𝑤 = 𝑋 → ⟨𝑤, 𝑣⟩ = ⟨𝑋, 𝑣⟩)
3837oveq1d 7249 . . . . . . . . 9 (𝑤 = 𝑋 → (⟨𝑤, 𝑣· 𝑢) = (⟨𝑋, 𝑣· 𝑢))
3938oveqd 7251 . . . . . . . 8 (𝑤 = 𝑋 → (𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑣· 𝑢)𝑘))
40 oveq1 7241 . . . . . . . 8 (𝑤 = 𝑋 → (𝑤𝐻𝑢) = (𝑋𝐻𝑢))
4139, 40eleq12d 2834 . . . . . . 7 (𝑤 = 𝑋 → ((𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
4241ralbidv 3120 . . . . . 6 (𝑤 = 𝑋 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
4336, 42raleqbidv 3327 . . . . 5 (𝑤 = 𝑋 → (∀𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
44 oveq2 7242 . . . . . 6 (𝑣 = 𝑌 → (𝑋𝐻𝑣) = (𝑋𝐻𝑌))
45 oveq1 7241 . . . . . . 7 (𝑣 = 𝑌 → (𝑣𝐻𝑢) = (𝑌𝐻𝑢))
46 opeq2 4801 . . . . . . . . . 10 (𝑣 = 𝑌 → ⟨𝑋, 𝑣⟩ = ⟨𝑋, 𝑌⟩)
4746oveq1d 7249 . . . . . . . . 9 (𝑣 = 𝑌 → (⟨𝑋, 𝑣· 𝑢) = (⟨𝑋, 𝑌· 𝑢))
4847oveqd 7251 . . . . . . . 8 (𝑣 = 𝑌 → (𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌· 𝑢)𝑘))
4948eleq1d 2824 . . . . . . 7 (𝑣 = 𝑌 → ((𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
5045, 49raleqbidv 3327 . . . . . 6 (𝑣 = 𝑌 → (∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
5144, 50raleqbidv 3327 . . . . 5 (𝑣 = 𝑌 → (∀𝑘 ∈ (𝑋𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑋, 𝑣· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢)))
52 oveq2 7242 . . . . . . 7 (𝑢 = 𝑍 → (𝑌𝐻𝑢) = (𝑌𝐻𝑍))
53 oveq2 7242 . . . . . . . . 9 (𝑢 = 𝑍 → (⟨𝑋, 𝑌· 𝑢) = (⟨𝑋, 𝑌· 𝑍))
5453oveqd 7251 . . . . . . . 8 (𝑢 = 𝑍 → (𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) = (𝑙(⟨𝑋, 𝑌· 𝑍)𝑘))
55 oveq2 7242 . . . . . . . 8 (𝑢 = 𝑍 → (𝑋𝐻𝑢) = (𝑋𝐻𝑍))
5654, 55eleq12d 2834 . . . . . . 7 (𝑢 = 𝑍 → ((𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ (𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
5752, 56raleqbidv 3327 . . . . . 6 (𝑢 = 𝑍 → (∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
5857ralbidv 3120 . . . . 5 (𝑢 = 𝑍 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑢)(𝑙(⟨𝑋, 𝑌· 𝑢)𝑘) ∈ (𝑋𝐻𝑢) ↔ ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
5943, 51, 58rspc3v 3564 . . . 4 ((𝑋𝐵𝑌𝐵𝑍𝐵) → (∀𝑤𝐵𝑣𝐵𝑢𝐵𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
6033, 34, 35, 59syl3anc 1373 . . 3 (𝜑 → (∀𝑤𝐵𝑣𝐵𝑢𝐵𝑘 ∈ (𝑤𝐻𝑣)∀𝑙 ∈ (𝑣𝐻𝑢)(𝑙(⟨𝑤, 𝑣· 𝑢)𝑘) ∈ (𝑤𝐻𝑢) → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍)))
6132, 60mpd 15 . 2 (𝜑 → ∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍))
62 isthincd2lem2.4 . . 3 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
63 isthincd2lem2.5 . . 3 (𝜑𝐺 ∈ (𝑌𝐻𝑍))
64 oveq2 7242 . . . . 5 (𝑘 = 𝐹 → (𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) = (𝑙(⟨𝑋, 𝑌· 𝑍)𝐹))
6564eleq1d 2824 . . . 4 (𝑘 = 𝐹 → ((𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍) ↔ (𝑙(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
66 oveq1 7241 . . . . 5 (𝑙 = 𝐺 → (𝑙(⟨𝑋, 𝑌· 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))
6766eleq1d 2824 . . . 4 (𝑙 = 𝐺 → ((𝑙(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍) ↔ (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
6865, 67rspc2v 3561 . . 3 ((𝐹 ∈ (𝑋𝐻𝑌) ∧ 𝐺 ∈ (𝑌𝐻𝑍)) → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
6962, 63, 68syl2anc 587 . 2 (𝜑 → (∀𝑘 ∈ (𝑋𝐻𝑌)∀𝑙 ∈ (𝑌𝐻𝑍)(𝑙(⟨𝑋, 𝑌· 𝑍)𝑘) ∈ (𝑋𝐻𝑍) → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍)))
7061, 69mpd 15 1 (𝜑 → (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  wral 3063  cop 4563  (class class class)co 7234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-iota 6358  df-fv 6408  df-ov 7237
This theorem is referenced by:  isthincd2  46025
  Copyright terms: Public domain W3C validator