Metamath Proof Explorer

Theorem dihoml4c

Description: Version of dihoml4 with closed subspaces. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihoml4c.h ⊢ H = LHyp ⁡ K
dihoml4c.i ⊢ I = DIsoH ⁡ K ⁡ W
dihoml4c.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dihoml4c.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihoml4c.x ⊢ φ → X ∈ ran ⁡ I
dihoml4c.y ⊢ φ → Y ∈ ran ⁡ I
dihoml4c.l ⊢ φ → X ⊆ Y
Assertion dihoml4c ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = X

Proof

Step Hyp Ref Expression
1 dihoml4c.h ⊢ H = LHyp ⁡ K
2 dihoml4c.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dihoml4c.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 dihoml4c.k ⊢ φ → K ∈ HL ∧ W ∈ H
5 dihoml4c.x ⊢ φ → X ∈ ran ⁡ I
6 dihoml4c.y ⊢ φ → Y ∈ ran ⁡ I
7 dihoml4c.l ⊢ φ → X ⊆ Y
8 eqid ⊢ meet ⁡ K = meet ⁡ K
9 inss1 ⊢ ⊥ ˙ ⁡ X ∩ Y ⊆ ⊥ ˙ ⁡ X
10 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
11 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
12 1 10 2 11 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ Base DVecH ⁡ K ⁡ W
13 4 5 12 syl2anc ⊢ φ → X ⊆ Base DVecH ⁡ K ⁡ W
14 1 10 11 3 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ Base DVecH ⁡ K ⁡ W → ⊥ ˙ ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
15 4 13 14 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
16 9 15 sstrid ⊢ φ → ⊥ ˙ ⁡ X ∩ Y ⊆ Base DVecH ⁡ K ⁡ W
17 1 2 10 11 3 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∩ Y ⊆ Base DVecH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∈ ran ⁡ I
18 4 16 17 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∈ ran ⁡ I
19 8 1 2 4 18 6 dihmeet2 ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y meet ⁡ K I -1 ⁡ Y
20 eqid ⊢ oc ⁡ K = oc ⁡ K
21 1 2 10 11 3 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ Base DVecH ⁡ K ⁡ W → ⊥ ˙ ⁡ X ∈ ran ⁡ I
22 4 13 21 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ I
23 1 2 dihmeetcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → ⊥ ˙ ⁡ X ∩ Y ∈ ran ⁡ I
24 4 22 6 23 syl12anc ⊢ φ → ⊥ ˙ ⁡ X ∩ Y ∈ ran ⁡ I
25 20 1 2 3 4 24 dochvalr3 ⊢ φ → oc ⁡ K ⁡ I -1 ⁡ ⊥ ˙ ⁡ X ∩ Y = I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y
26 8 1 2 4 22 6 dihmeet2 ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ X ∩ Y = I -1 ⁡ ⊥ ˙ ⁡ X meet ⁡ K I -1 ⁡ Y
27 20 1 2 3 4 5 dochvalr3 ⊢ φ → oc ⁡ K ⁡ I -1 ⁡ X = I -1 ⁡ ⊥ ˙ ⁡ X
28 27 oveq1d ⊢ φ → oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y = I -1 ⁡ ⊥ ˙ ⁡ X meet ⁡ K I -1 ⁡ Y
29 26 28 eqtr4d ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ X ∩ Y = oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y
30 29 fveq2d ⊢ φ → oc ⁡ K ⁡ I -1 ⁡ ⊥ ˙ ⁡ X ∩ Y = oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y
31 25 30 eqtr3d ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y = oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y
32 31 oveq1d ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y meet ⁡ K I -1 ⁡ Y = oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y meet ⁡ K I -1 ⁡ Y
33 eqid ⊢ ≤ K = ≤ K
34 33 1 2 4 5 6 dihcnvord ⊢ φ → I -1 ⁡ X ≤ K I -1 ⁡ Y ↔ X ⊆ Y
35 7 34 mpbird ⊢ φ → I -1 ⁡ X ≤ K I -1 ⁡ Y
36 4 simpld ⊢ φ → K ∈ HL
37 hloml ⊢ K ∈ HL → K ∈ OML
38 36 37 syl ⊢ φ → K ∈ OML
39 eqid ⊢ Base K = Base K
40 39 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
41 4 5 40 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
42 39 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
43 4 6 42 syl2anc ⊢ φ → I -1 ⁡ Y ∈ Base K
44 39 33 8 20 omllaw4 ⊢ K ∈ OML ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I -1 ⁡ X ≤ K I -1 ⁡ Y → oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y meet ⁡ K I -1 ⁡ Y = I -1 ⁡ X
45 38 41 43 44 syl3anc ⊢ φ → I -1 ⁡ X ≤ K I -1 ⁡ Y → oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y meet ⁡ K I -1 ⁡ Y = I -1 ⁡ X
46 35 45 mpd ⊢ φ → oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y meet ⁡ K I -1 ⁡ Y = I -1 ⁡ X
47 19 32 46 3eqtrd ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = I -1 ⁡ X
48 1 2 dihmeetcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y ∈ ran ⁡ I
49 4 18 6 48 syl12anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y ∈ ran ⁡ I
50 1 2 4 49 5 dihcnv11 ⊢ φ → I -1 ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = I -1 ⁡ X ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = X
51 47 50 mpbid ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = X