# Metamath Proof Explorer

## Theorem dihf11lem

Description: Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihf11.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihf11.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihf11.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihf11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihf11.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion dihf11lem ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}⟶{S}$

### Proof

Step Hyp Ref Expression
1 dihf11.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihf11.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dihf11.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dihf11.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dihf11.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 fvex ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right)\in \mathrm{V}$
7 riotaex ${⊢}\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\in \mathrm{V}$
8 6 7 ifex ${⊢}if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\in \mathrm{V}$
9 8 rgenw ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\in \mathrm{V}$
10 9 a1i ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\in \mathrm{V}$
11 eqid ${⊢}\left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)=\left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)$
12 11 mptfng ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\in \mathrm{V}↔\left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)Fn{B}$
13 10 12 sylib ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)Fn{B}$
14 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
15 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
16 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
17 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
18 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
19 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
20 eqid ${⊢}\mathrm{LSSum}\left({U}\right)=\mathrm{LSSum}\left({U}\right)$
21 1 14 15 16 17 2 3 18 19 4 5 20 dihfval ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}=\left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)$
22 21 fneq1d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({I}Fn{B}↔\left({x}\in {B}⟼if\left({x}{\le }_{{K}}{W},\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\right),\left(\iota {u}\in {S}|\forall {q}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left(\left(¬{q}{\le }_{{K}}{W}\wedge {q}\mathrm{join}\left({K}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)={x}\right)\to {u}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({q}\right)\mathrm{LSSum}\left({U}\right)\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({x}\mathrm{meet}\left({K}\right){W}\right)\right)\right)\right)\right)Fn{B}\right)$
23 13 22 mpbird ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn{B}$
24 1 2 3 4 5 dihlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {y}\in {B}\right)\to {I}\left({y}\right)\in {S}$
25 24 ralrimiva ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)\in {S}$
26 fnfvrnss ${⊢}\left({I}Fn{B}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{I}\left({y}\right)\in {S}\right)\to \mathrm{ran}{I}\subseteq {S}$
27 23 25 26 syl2anc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ran}{I}\subseteq {S}$
28 df-f ${⊢}{I}:{B}⟶{S}↔\left({I}Fn{B}\wedge \mathrm{ran}{I}\subseteq {S}\right)$
29 23 27 28 sylanbrc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}⟶{S}$