| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dihf11.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
dihf11.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 3 |
|
dihf11.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
| 4 |
|
dihf11.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
| 5 |
|
dihf11.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
| 6 |
|
fvex |
⊢ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∈ V |
| 7 |
|
riotaex |
⊢ ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ∈ V |
| 8 |
6 7
|
ifex |
⊢ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V |
| 9 |
8
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V |
| 10 |
9
|
a1i |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V ) |
| 11 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) |
| 12 |
11
|
mptfng |
⊢ ( ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V ↔ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 ) |
| 13 |
10 12
|
sylib |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 ) |
| 14 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 15 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 16 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
| 17 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 18 |
|
eqid |
⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) |
| 19 |
|
eqid |
⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) |
| 20 |
|
eqid |
⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 ) |
| 21 |
1 14 15 16 17 2 3 18 19 4 5 20
|
dihfval |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) ) |
| 22 |
21
|
fneq1d |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn 𝐵 ↔ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 ) ) |
| 23 |
13 22
|
mpbird |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn 𝐵 ) |
| 24 |
1 2 3 4 5
|
dihlss |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 ) |
| 25 |
24
|
ralrimiva |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑦 ∈ 𝐵 ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 ) |
| 26 |
|
fnfvrnss |
⊢ ( ( 𝐼 Fn 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 ) → ran 𝐼 ⊆ 𝑆 ) |
| 27 |
23 25 26
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 ) |
| 28 |
|
df-f |
⊢ ( 𝐼 : 𝐵 ⟶ 𝑆 ↔ ( 𝐼 Fn 𝐵 ∧ ran 𝐼 ⊆ 𝑆 ) ) |
| 29 |
23 27 28
|
sylanbrc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 ⟶ 𝑆 ) |