Metamath Proof Explorer

Theorem dochffval

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
Assertion dochffval ⊢ K ∈ V → ocH ⁡ K = w ∈ H ⟼ x ∈ 𝒫 Base DVecH ⁡ K ⁡ w ⟼ DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ 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 elex ⊢ K ∈ V → K ∈ V
6 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
7 6 4 eqtr4di ⊢ k = K → LHyp ⁡ k = H
8 fveq2 ⊢ k = K → DVecH ⁡ k = DVecH ⁡ K
9 8 fveq1d ⊢ k = K → DVecH ⁡ k ⁡ w = DVecH ⁡ K ⁡ w
10 9 fveq2d ⊢ k = K → Base DVecH ⁡ k ⁡ w = Base DVecH ⁡ K ⁡ w
11 10 pweqd ⊢ k = K → 𝒫 Base DVecH ⁡ k ⁡ w = 𝒫 Base DVecH ⁡ K ⁡ w
12 fveq2 ⊢ k = K → DIsoH ⁡ k = DIsoH ⁡ K
13 12 fveq1d ⊢ k = K → DIsoH ⁡ k ⁡ w = DIsoH ⁡ K ⁡ w
14 fveq2 ⊢ k = K → oc ⁡ k = oc ⁡ K
15 14 3 eqtr4di ⊢ k = K → oc ⁡ k = ⊥ ˙
16 fveq2 ⊢ k = K → glb ⁡ k = glb ⁡ K
17 16 2 eqtr4di ⊢ k = K → glb ⁡ k = G
18 fveq2 ⊢ k = K → Base k = Base K
19 18 1 eqtr4di ⊢ k = K → Base k = B
20 13 fveq1d ⊢ k = K → DIsoH ⁡ k ⁡ w ⁡ y = DIsoH ⁡ K ⁡ w ⁡ y
21 20 sseq2d ⊢ k = K → x ⊆ DIsoH ⁡ k ⁡ w ⁡ y ↔ x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
22 19 21 rabeqbidv ⊢ k = K → y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
23 17 22 fveq12d ⊢ k = K → glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
24 15 23 fveq12d ⊢ k = K → oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
25 13 24 fveq12d ⊢ k = K → DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
26 11 25 mpteq12dv ⊢ k = K → x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = x ∈ 𝒫 Base DVecH ⁡ K ⁡ w ⟼ DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
27 7 26 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y = w ∈ H ⟼ x ∈ 𝒫 Base DVecH ⁡ K ⁡ w ⟼ DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
28 df-doch ⊢ ocH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ DIsoH ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ glb ⁡ k ⁡ y ∈ Base k | x ⊆ DIsoH ⁡ k ⁡ w ⁡ y
29 27 28 4 mptfvmpt ⊢ K ∈ V → ocH ⁡ K = w ∈ H ⟼ x ∈ 𝒫 Base DVecH ⁡ K ⁡ w ⟼ DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y
30 5 29 syl ⊢ K ∈ V → ocH ⁡ K = w ∈ H ⟼ x ∈ 𝒫 Base DVecH ⁡ K ⁡ w ⟼ DIsoH ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ G ⁡ y ∈ B | x ⊆ DIsoH ⁡ K ⁡ w ⁡ y