| Step | Hyp | Ref
| Expression |
| 1 | | dihval.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 2 | | dihval.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
| 3 | | dihval.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
| 4 | | dihval.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
| 5 | | dihval.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
| 6 | | dihval.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 7 | | dihval.i |
. . . 4
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
| 8 | | dihval.d |
. . . 4
⊢ 𝐷 = ((DIsoB‘𝐾)‘𝑊) |
| 9 | | dihval.c |
. . . 4
⊢ 𝐶 = ((DIsoC‘𝐾)‘𝑊) |
| 10 | | dihval.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 11 | | dihval.s |
. . . 4
⊢ 𝑆 = (LSubSp‘𝑈) |
| 12 | | dihval.p |
. . . 4
⊢ ⊕ =
(LSSum‘𝑈) |
| 13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | dihfval 41233 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))))))) |
| 14 | 13 | fveq1d 6908 |
. 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝐼‘𝑋) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))))))‘𝑋)) |
| 15 | | breq1 5146 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊)) |
| 16 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐷‘𝑥) = (𝐷‘𝑋)) |
| 17 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥 ∧ 𝑊) = (𝑋 ∧ 𝑊)) |
| 18 | 17 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑞 ∨ (𝑋 ∧ 𝑊))) |
| 19 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
| 20 | 18, 19 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥 ↔ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) |
| 21 | 20 | anbi2d 630 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) ↔ (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋))) |
| 22 | | fvoveq1 7454 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐷‘(𝑥 ∧ 𝑊)) = (𝐷‘(𝑋 ∧ 𝑊))) |
| 23 | 22 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))) = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))) |
| 24 | 23 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))) ↔ 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))) |
| 25 | 21, 24 | imbi12d 344 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))) ↔ ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))))) |
| 26 | 25 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = 𝑋 → (∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))) ↔ ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))))) |
| 27 | 26 | riotabidv 7390 |
. . . 4
⊢ (𝑥 = 𝑋 → (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))))) = (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))))) |
| 28 | 15, 16, 27 | ifbieq12d 4554 |
. . 3
⊢ (𝑥 = 𝑋 → if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))))) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))))) |
| 29 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))))))) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊))))))) |
| 30 | | fvex 6919 |
. . . 4
⊢ (𝐷‘𝑋) ∈ V |
| 31 | | riotaex 7392 |
. . . 4
⊢
(℩𝑢
∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))) ∈ V |
| 32 | 30, 31 | ifex 4576 |
. . 3
⊢ if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊)))))) ∈ V |
| 33 | 28, 29, 32 | fvmpt 7016 |
. 2
⊢ (𝑋 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ≤ 𝑊, (𝐷‘𝑥), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑥 ∧ 𝑊)))))))‘𝑋) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))))) |
| 34 | 14, 33 | sylan9eq 2797 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) = if(𝑋 ≤ 𝑊, (𝐷‘𝑋), (℩𝑢 ∈ 𝑆 ∀𝑞 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → 𝑢 = ((𝐶‘𝑞) ⊕ (𝐷‘(𝑋 ∧ 𝑊))))))) |