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 ‘ 𝐾 )
docaval.m ⊢ ∧ = ( meet ‘ 𝐾 )
docaval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
docaval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion docaffvalN ( 𝐾 ∈ 𝑉 → ( ocA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 docaval.j ⊢ ∨ = ( join ‘ 𝐾 )
2 docaval.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 docaval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
4 docaval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
7 6 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
9 8 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
10 9 pweqd ⊢ ( 𝑘 = 𝐾 → 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
11 fveq2 ⊢ ( 𝑘 = 𝐾 → ( DIsoA ‘ 𝑘 ) = ( DIsoA ‘ 𝐾 ) )
12 11 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) )
13 fveq2 ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ( meet ‘ 𝐾 ) )
14 13 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ∧ )
15 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
16 15 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
17 fveq2 ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ( oc ‘ 𝐾 ) )
18 17 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ⊥ )
19 12 cnveqd ⊢ ( 𝑘 = 𝐾 → ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) = ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) )
20 12 rneqd ⊢ ( 𝑘 = 𝐾 → ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) = ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) )
21 20 rabeqdv ⊢ ( 𝑘 = 𝐾 → { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } = { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } )
22 21 inteqd ⊢ ( 𝑘 = 𝐾 → ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } = ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } )
23 19 22 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) = ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) )
24 18 23 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) = ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) )
25 18 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) = ( ⊥ ‘ 𝑤 ) )
26 16 24 25 oveq123d ⊢ ( 𝑘 = 𝐾 → ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) )
27 eqidd ⊢ ( 𝑘 = 𝐾 → 𝑤 = 𝑤 )
28 14 26 27 oveq123d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) = ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) )
29 12 28 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) = ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) )
30 10 29 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) = ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) ) )
31 7 30 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) ) ) )
32 df-docaN ⊢ ocA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )
33 31 32 4 mptfvmpt ⊢ ( 𝐾 ∈ V → ( ocA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) ) ) )
34 5 33 syl ⊢ ( 𝐾 ∈ 𝑉 → ( ocA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ⊥ ‘ ( ◡ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑤 ) ) ∧ 𝑤 ) ) ) ) )