Metamath Proof Explorer

Theorem docavalN

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 docavalN ⊢K∈HL∧W∈H∧X⊆T→N⁡X=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 5 6 7 docafvalN ⊢K∈HL∧W∈H→N=x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W
9 8 adantr ⊢K∈HL∧W∈H∧X⊆T→N=x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W
10 9 fveq1d ⊢K∈HL∧W∈H∧X⊆T→N⁡X=x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W⁡X
11 5 fvexi ⊢T∈V
12 11 elpw2 ⊢X∈𝒫T↔X⊆T
13 12 biimpri ⊢X⊆T→X∈𝒫T
14 13 adantl ⊢K∈HL∧W∈H∧X⊆T→X∈𝒫T
15 fvex ⊢I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W∈V
16 sseq1 ⊢x=X→x⊆z↔X⊆z
17 16 rabbidv ⊢x=X→z∈ran⁡I|x⊆z=z∈ran⁡I|X⊆z
18 17 inteqd ⊢x=X→⋂z∈ran⁡I|x⊆z=⋂z∈ran⁡I|X⊆z
19 18 fveq2d ⊢x=X→I-1⁡⋂z∈ran⁡I|x⊆z=I-1⁡⋂z∈ran⁡I|X⊆z
20 19 fveq2d ⊢x=X→⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z=⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z
21 20 oveq1d ⊢x=X→⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W=⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W
22 21 fvoveq1d ⊢x=X→I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W=I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W
23 eqid ⊢x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W=x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W
24 22 23 fvmptg ⊢X∈𝒫T∧I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W∈V→x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W⁡X=I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W
25 14 15 24 sylancl ⊢K∈HL∧W∈H∧X⊆T→x∈𝒫T⟼I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|x⊆z∨˙⊥˙⁡W∧˙W⁡X=I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W
26 10 25 eqtrd ⊢K∈HL∧W∈H∧X⊆T→N⁡X=I⁡⊥˙⁡I-1⁡⋂z∈ran⁡I|X⊆z∨˙⊥˙⁡W∧˙W