Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemk7.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
cdlemk7.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
cdlemk7.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
cdlemk7.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
6 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
7 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
8 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
9 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
10 |
|
eqid |
⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) |
11 |
|
eqid |
⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) |
12 |
|
eqid |
⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) |
13 |
|
eqid |
⊢ ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) = ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) |
14 |
|
eqid |
⊢ ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) |
15 |
5 6 7 8 9 1 2 3 10 11 12 13 14 4
|
cdlemk56w |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) → ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ∈ 𝐸 ∧ ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ‘ 𝐹 ) = 𝑁 ) ) |
16 |
|
fveq1 |
⊢ ( 𝑢 = ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) → ( 𝑢 ‘ 𝐹 ) = ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ‘ 𝐹 ) ) |
17 |
16
|
eqeq1d |
⊢ ( 𝑢 = ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) → ( ( 𝑢 ‘ 𝐹 ) = 𝑁 ↔ ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ‘ 𝐹 ) = 𝑁 ) ) |
18 |
17
|
rspcev |
⊢ ( ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ∈ 𝐸 ∧ ( ( 𝑓 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑓 , ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑓 ) ) → ( 𝑧 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑓 ) ) ( meet ‘ 𝐾 ) ( ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑏 ) ) ( meet ‘ 𝐾 ) ( ( 𝑁 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑏 ∘ ◡ 𝐹 ) ) ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝑏 ) ) ) ) ) ) ) ) ‘ 𝐹 ) = 𝑁 ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 ) |
19 |
15 18
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 ) |