Metamath Proof Explorer

Theorem docafvalN

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
docaval.t ⊢ T = LTrn ⁡ K ⁡ W
docaval.i ⊢ I = DIsoA ⁡ K ⁡ W
docaval.n ⊢ N = ocA ⁡ K ⁡ W
Assertion docafvalN ⊢ K ∈ V ∧ W ∈ H → N = x ∈ 𝒫 T ⟼ I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | 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 docaval.t ⊢ T = LTrn ⁡ K ⁡ W
6 docaval.i ⊢ I = DIsoA ⁡ K ⁡ W
7 docaval.n ⊢ N = ocA ⁡ K ⁡ W
8 1 2 3 4 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
9 8 fveq1d ⊢ K ∈ V → ocA ⁡ K ⁡ W = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w ⁡ W
10 7 9 syl5eq ⊢ K ∈ V → N = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w ⁡ W
11 fveq2 ⊢ w = W → LTrn ⁡ K ⁡ w = LTrn ⁡ K ⁡ W
12 11 5 eqtr4di ⊢ w = W → LTrn ⁡ K ⁡ w = T
13 12 pweqd ⊢ w = W → 𝒫 LTrn ⁡ K ⁡ w = 𝒫 T
14 fveq2 ⊢ w = W → DIsoA ⁡ K ⁡ w = DIsoA ⁡ K ⁡ W
15 14 6 eqtr4di ⊢ w = W → DIsoA ⁡ K ⁡ w = I
16 15 cnveqd ⊢ w = W → DIsoA ⁡ K ⁡ w -1 = I -1
17 15 rneqd ⊢ w = W → ran ⁡ DIsoA ⁡ K ⁡ w = ran ⁡ I
18 17 rabeqdv ⊢ w = W → z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z = z ∈ ran ⁡ I | x ⊆ z
19 18 inteqd ⊢ w = W → ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z = ⋂ z ∈ ran ⁡ I | x ⊆ z
20 16 19 fveq12d ⊢ w = W → DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z = I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z
21 20 fveq2d ⊢ w = W → ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z = ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z
22 fveq2 ⊢ w = W → ⊥ ˙ ⁡ w = ⊥ ˙ ⁡ W
23 21 22 oveq12d ⊢ w = W → ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w = ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W
24 id ⊢ w = W → w = W
25 23 24 oveq12d ⊢ w = W → ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w = ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W
26 15 25 fveq12d ⊢ w = W → DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W
27 13 26 mpteq12dv ⊢ w = W → x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w = x ∈ 𝒫 T ⟼ I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W
28 eqid ⊢ w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w = w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w
29 5 fvexi ⊢ T ∈ V
30 29 pwex ⊢ 𝒫 T ∈ V
31 30 mptex ⊢ x ∈ 𝒫 T ⟼ I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W ∈ V
32 27 28 31 fvmpt ⊢ W ∈ H → w ∈ H ⟼ x ∈ 𝒫 LTrn ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ ⊥ ˙ ⁡ DIsoA ⁡ K ⁡ w -1 ⁡ ⋂ z ∈ ran ⁡ DIsoA ⁡ K ⁡ w | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ w ∧ ˙ w ⁡ W = x ∈ 𝒫 T ⟼ I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W
33 10 32 sylan9eq ⊢ K ∈ V ∧ W ∈ H → N = x ∈ 𝒫 T ⟼ I ⁡ ⊥ ˙ ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | x ⊆ z ∨ ˙ ⊥ ˙ ⁡ W ∧ ˙ W