Metamath Proof Explorer

Theorem dochval2

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Apr-2014)

Ref Expression
Hypotheses dochval2.o
dochval2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochval2.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dochval2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochval2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochval2.n ${⊢}{N}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
Assertion dochval2

Proof

Step Hyp Ref Expression
1 dochval2.o
2 dochval2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dochval2.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dochval2.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dochval2.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 dochval2.n ${⊢}{N}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
8 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
9 7 8 1 2 3 4 5 6 dochval
10 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
11 10 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {K}\in \mathrm{CLat}$
12 ssrab2 ${⊢}\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}$
13 7 8 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge \left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}$
14 11 12 13 sylancl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}$
15 7 2 3 dihcnvid1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}\right)\to {{I}}^{-1}\left({I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\right)\right)=\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)$
16 14 15 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {{I}}^{-1}\left({I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\right)\right)=\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)$
17 7 8 2 3 4 5 dihglb2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\right)=\bigcap \left\{{z}\in \mathrm{ran}{I}|{X}\subseteq {z}\right\}$
18 17 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {{I}}^{-1}\left({I}\left(\mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)\right)\right)={{I}}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}{I}|{X}\subseteq {z}\right\}\right)$
19 16 18 eqtr3d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{x}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({x}\right)\right\}\right)={{I}}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}{I}|{X}\subseteq {z}\right\}\right)$
20 19 fveq2d
21 20 fveq2d
22 9 21 eqtrd