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 ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W
9 1 3 diaf11N ⊢ K ∈ HL ∧ W ∈ H → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
10 f1ofun ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ 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 ⊢ Base K = Base K
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 ∈ Base K
32 29 31 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
33 30 7 opoccl ⊢ K ∈ OP ∧ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
34 16 32 33 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
35 30 1 lhpbase ⊢ W ∈ H → W ∈ Base K
36 35 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → W ∈ Base K
37 30 7 opoccl ⊢ K ∈ OP ∧ W ∈ Base K → oc ⁡ K ⁡ W ∈ Base K
38 16 36 37 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ W ∈ Base K
39 30 5 latjcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K ∧ oc ⁡ K ⁡ W ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W ∈ Base K
40 14 34 38 39 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W ∈ Base K
41 30 6 latmcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W ∈ Base K ∧ W ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K
42 14 40 36 41 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K
43 eqid ⊢ ≤ K = ≤ K
44 30 43 6 latmle2 ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W ∈ Base K ∧ W ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
45 14 40 36 44 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
46 30 43 1 3 diaeldm ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I ↔ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
47 46 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I ↔ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
48 42 45 47 mpbir2and ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I
49 fvelrn ⊢ Fun ⁡ I ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I → I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ ran ⁡ I
50 12 48 49 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ ran ⁡ I
51 8 50 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ T → ⊥ ˙ ⁡ X ∈ ran ⁡ I