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 ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) )