Metamath Proof Explorer

Theorem dochval

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

Ref Expression
Hypotheses dochval.b ⊢ B = Base K
dochval.g ⊢ G = glb ⁡ K
dochval.o ⊢ ⊥ ˙ = oc ⁡ K
dochval.h ⊢ H = LHyp ⁡ K
dochval.i ⊢ I = DIsoH ⁡ K ⁡ W
dochval.u ⊢ U = DVecH ⁡ K ⁡ W
dochval.v ⊢ V = Base U
dochval.n ⊢ N = ocH ⁡ K ⁡ W
Assertion dochval ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y

Proof

Step Hyp Ref Expression
1 dochval.b ⊢ B = Base K
2 dochval.g ⊢ G = glb ⁡ K
3 dochval.o ⊢ ⊥ ˙ = oc ⁡ K
4 dochval.h ⊢ H = LHyp ⁡ K
5 dochval.i ⊢ I = DIsoH ⁡ K ⁡ W
6 dochval.u ⊢ U = DVecH ⁡ K ⁡ W
7 dochval.v ⊢ V = Base U
8 dochval.n ⊢ N = ocH ⁡ K ⁡ W
9 1 2 3 4 5 6 7 8 dochfval ⊢ K ∈ Y ∧ W ∈ H → N = x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y
10 9 adantr ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → N = x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y
11 10 fveq1d ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y ⁡ X
12 7 fvexi ⊢ V ∈ V
13 12 elpw2 ⊢ X ∈ 𝒫 V ↔ X ⊆ V
14 13 biimpri ⊢ X ⊆ V → X ∈ 𝒫 V
15 14 adantl ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → X ∈ 𝒫 V
16 fvex ⊢ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y ∈ V
17 sseq1 ⊢ x = X → x ⊆ I ⁡ y ↔ X ⊆ I ⁡ y
18 17 rabbidv ⊢ x = X → y ∈ B | x ⊆ I ⁡ y = y ∈ B | X ⊆ I ⁡ y
19 18 fveq2d ⊢ x = X → G ⁡ y ∈ B | x ⊆ I ⁡ y = G ⁡ y ∈ B | X ⊆ I ⁡ y
20 19 fveq2d ⊢ x = X → ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y = ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y
21 20 fveq2d ⊢ x = X → I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y = I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y
22 eqid ⊢ x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y = x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y
23 21 22 fvmptg ⊢ X ∈ 𝒫 V ∧ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y ∈ V → x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y ⁡ X = I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y
24 15 16 23 sylancl ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → x ∈ 𝒫 V ⟼ I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ I ⁡ y ⁡ X = I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y
25 11 24 eqtrd ⊢ K ∈ Y ∧ W ∈ H ∧ X ⊆ V → N ⁡ X = I ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | X ⊆ I ⁡ y