Metamath Proof Explorer

Theorem dochval2

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

Ref Expression
Hypotheses dochval2.o ⊢ ⊥ ˙ = oc ⁡ K
dochval2.h ⊢ H = LHyp ⁡ K
dochval2.i ⊢ I = DIsoH ⁡ K ⁡ W
dochval2.u ⊢ U = DVecH ⁡ K ⁡ W
dochval2.v ⊢ V = Base U
dochval2.n ⊢ N = ocH ⁡ K ⁡ W
Assertion dochval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z

Proof

Step Hyp Ref Expression
1 dochval2.o ⊢ ⊥ ˙ = oc ⁡ K
2 dochval2.h ⊢ H = LHyp ⁡ K
3 dochval2.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dochval2.u ⊢ U = DVecH ⁡ K ⁡ W
5 dochval2.v ⊢ V = Base U
6 dochval2.n ⊢ N = ocH ⁡ K ⁡ W
7 eqid ⊢ Base K = Base K
8 eqid ⊢ glb ⁡ K = glb ⁡ K
9 7 8 1 2 3 4 5 6 dochval ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = I ⁡ ⊥ ˙ ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x
10 hlclat ⊢ K ∈ HL → K ∈ CLat
11 10 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → K ∈ CLat
12 ssrab2 ⊢ x ∈ Base K | X ⊆ I ⁡ x ⊆ Base K
13 7 8 clatglbcl ⊢ K ∈ CLat ∧ x ∈ Base K | X ⊆ I ⁡ x ⊆ Base K → glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x ∈ Base K
14 11 12 13 sylancl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x ∈ Base K
15 7 2 3 dihcnvid1 ⊢ K ∈ HL ∧ W ∈ H ∧ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x ∈ Base K → I -1 ⁡ I ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x
16 14 15 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → I -1 ⁡ I ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x
17 7 8 2 3 4 5 dihglb2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → I ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = ⋂ z ∈ ran ⁡ I | X ⊆ z
18 17 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → I -1 ⁡ I ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
19 16 18 eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
20 19 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
21 20 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → I ⁡ ⊥ ˙ ⁡ glb ⁡ K ⁡ x ∈ Base K | X ⊆ I ⁡ x = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
22 9 21 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z