Metamath Proof Explorer

Theorem docaffvalN

Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses docaval.j ⊢ ∨ ˙ = join ⁡ K
docaval.m ⊢ ∧ ˙ = meet ⁡ K
docaval.o ⊢ ⊥ ˙ = oc ⁡ K
docaval.h ⊢ H = LHyp ⁡ K
Assertion docaffvalN ⊢ K ∈ V → ocA ⁡ K = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w

Proof

Step Hyp Ref Expression
1 docaval.j ⊢ ∨ ˙ = join ⁡ K
2 docaval.m ⊢ ∧ ˙ = meet ⁡ K
3 docaval.o ⊢ ⊥ ˙ = oc ⁡ K
4 docaval.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 → LTrn ⁡ k = LTrn ⁡ K
9 8 fveq1d ⊢ k = K → LTrn ⁡ k ⁡ w = LTrn ⁡ K ⁡ w
10 9 pweqd ⊢ k = K → 𝒫 LTrn ⁡ k ⁡ w = 𝒫 LTrn ⁡ K ⁡ w
11 fveq2 ⊢ k = K → DIsoA ⁡ k = DIsoA ⁡ K
12 11 fveq1d ⊢ k = K → DIsoA ⁡ k ⁡ w = DIsoA ⁡ K ⁡ w
13 fveq2 ⊢ k = K → meet ⁡ k = meet ⁡ K
14 13 2 eqtr4di ⊢ k = K → meet ⁡ k = ∧ ˙
15 fveq2 ⊢ k = K → join ⁡ k = join ⁡ K
16 15 1 eqtr4di ⊢ k = K → join ⁡ k = ∨ ˙
17 fveq2 ⊢ k = K → oc ⁡ k = oc ⁡ K
18 17 3 eqtr4di ⊢ k = K → oc ⁡ k = ⊥ ˙
19 12 cnveqd ⊢ k = K → DIsoA ⁡ k ⁡ w -1 = DIsoA ⁡ K ⁡ w -1
20 12 rneqd ⊢ k = K → ran ⁡ DIsoA ⁡ k ⁡ w = ran ⁡ DIsoA ⁡ K ⁡ w
21 20 rabeqdv ⊢ k = K → z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z = z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z
22 21 inteqd ⊢ k = K → ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z = ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z
23 19 22 fveq12d ⊢ k = K → DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z = DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z
24 18 23 fveq12d ⊢ k = K → oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z = ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z
25 18 fveq1d ⊢ k = K → oc ⁡ k ⁡ w = ⊥ ˙ ⁡ w
26 16 24 25 oveq123d ⊢ k = K → oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w = ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w
27 eqidd ⊢ k = K → w = w
28 14 26 27 oveq123d ⊢ k = K → oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w = ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
29 12 28 fveq12d ⊢ k = K → DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w = DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
30 10 29 mpteq12dv ⊢ k = K → x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w = x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
31 7 30 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
32 df-docaN ⊢ ocA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ oc ⁡ k ⁡ DIsoA ⁡ k ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ k ⁡ w | x ⊆ z join ⁡ k oc ⁡ k ⁡ w meet ⁡ k w
33 31 32 4 mptfvmpt ⊢ K ∈ V → ocA ⁡ K = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
34 5 33 syl ⊢ K ∈ V → ocA ⁡ K = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w