Metamath Proof Explorer

Theorem docaclN

Description: Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses docacl.h ⊢H=LHyp⁡K
docacl.t ⊢T=LTrn⁡K⁡W
docacl.i ⊢I=DIsoA⁡K⁡W
docacl.n ⊢⊥˙=ocA⁡K⁡W
Assertion docaclN ⊢K∈HL∧W∈H∧X⊆T→⊥˙⁡X∈ran⁡I

Proof

Step Hyp Ref Expression
1 docacl.h ⊢H=LHyp⁡K
2 docacl.t ⊢T=LTrn⁡K⁡W
3 docacl.i ⊢I=DIsoA⁡K⁡W
4 docacl.n ⊢⊥˙=ocA⁡K⁡W
5 eqid ⊢join⁡K=join⁡K
6 eqid ⊢meet⁡K=meet⁡K
7 eqid ⊢oc⁡K=oc⁡K
8 5 6 7 1 2 3 4 docavalN ⊢K∈HL∧W∈H∧X⊆T→⊥˙⁡X=I⁡oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW
9 1 3 diaf11N ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1 ontoran⁡I
10 f1ofun ⊢I:dom⁡I⟶1-1 ontoran⁡I→Fun⁡I
11 9 10 syl ⊢K∈HL∧W∈H→Fun⁡I
12 11 adantr ⊢K∈HL∧W∈H∧X⊆T→Fun⁡I
13 hllat ⊢K∈HL→K∈Lat
14 13 ad2antrr ⊢K∈HL∧W∈H∧X⊆T→K∈Lat
15 hlop ⊢K∈HL→K∈OP
16 15 ad2antrr ⊢K∈HL∧W∈H∧X⊆T→K∈OP
17 simpl ⊢K∈HL∧W∈H∧X⊆T→K∈HL∧W∈H
18 ssrab2 ⊢z∈ran⁡I|X⊆z⊆ran⁡I
19 18 a1i ⊢K∈HL∧W∈H∧X⊆T→z∈ran⁡I|X⊆z⊆ran⁡I
20 1 2 3 dia1elN ⊢K∈HL∧W∈H→T∈ran⁡I
21 20 anim1i ⊢K∈HL∧W∈H∧X⊆T→T∈ran⁡I∧X⊆T
22 sseq2 ⊢z=T→X⊆z↔X⊆T
23 22 elrab ⊢T∈z∈ran⁡I|X⊆z↔T∈ran⁡I∧X⊆T
24 21 23 sylibr ⊢K∈HL∧W∈H∧X⊆T→T∈z∈ran⁡I|X⊆z
25 24 ne0d ⊢K∈HL∧W∈H∧X⊆T→z∈ran⁡I|X⊆z≠∅
26 1 3 diaintclN ⊢K∈HL∧W∈H∧z∈ran⁡I|X⊆z⊆ran⁡I∧z∈ran⁡I|X⊆z≠∅→⋂z∈ran⁡I|X⊆z∈ran⁡I
27 17 19 25 26 syl12anc ⊢K∈HL∧W∈H∧X⊆T→⋂z∈ran⁡I|X⊆z∈ran⁡I
28 1 3 diacnvclN ⊢K∈HL∧W∈H∧⋂z∈ran⁡I|X⊆z∈ran⁡I→I-1⁡⋂z∈ran⁡I|X⊆z∈dom⁡I
29 27 28 syldan ⊢K∈HL∧W∈H∧X⊆T→I-1⁡⋂z∈ran⁡I|X⊆z∈dom⁡I
30 eqid ⊢BaseK=BaseK
31 30 1 3 diadmclN ⊢K∈HL∧W∈H∧I-1⁡⋂z∈ran⁡I|X⊆z∈dom⁡I→I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK
32 29 31 syldan ⊢K∈HL∧W∈H∧X⊆T→I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK
33 30 7 opoccl ⊢K∈OP∧I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK
34 16 32 33 syl2anc ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK
35 30 1 lhpbase ⊢W∈H→W∈BaseK
36 35 ad2antlr ⊢K∈HL∧W∈H∧X⊆T→W∈BaseK
37 30 7 opoccl ⊢K∈OP∧W∈BaseK→oc⁡K⁡W∈BaseK
38 16 36 37 syl2anc ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡W∈BaseK
39 30 5 latjcl ⊢K∈Lat∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆z∈BaseK∧oc⁡K⁡W∈BaseK→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡W∈BaseK
40 14 34 38 39 syl3anc ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡W∈BaseK
41 30 6 latmcl ⊢K∈Lat∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡W∈BaseK∧W∈BaseK→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK
42 14 40 36 41 syl3anc ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK
43 eqid ⊢≤K=≤K
44 30 43 6 latmle2 ⊢K∈Lat∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡W∈BaseK∧W∈BaseK→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
45 14 40 36 44 syl3anc ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
46 30 43 1 3 diaeldm ⊢K∈HL∧W∈H→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I↔oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
47 46 adantr ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I↔oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
48 42 45 47 mpbir2and ⊢K∈HL∧W∈H∧X⊆T→oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I
49 fvelrn ⊢Fun⁡I∧oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I→I⁡oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈ran⁡I
50 12 48 49 syl2anc ⊢K∈HL∧W∈H∧X⊆T→I⁡oc⁡K⁡I-1⁡⋂z∈ran⁡I|X⊆zjoin⁡Koc⁡K⁡Wmeet⁡KW∈ran⁡I
51 8 50 eqeltrd ⊢K∈HL∧W∈H∧X⊆T→⊥˙⁡X∈ran⁡I