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 ‘ 𝐾 )
docaval.m = ( meet ‘ 𝐾 )
docaval.o = ( oc ‘ 𝐾 )
docaval.h 𝐻 = ( LHyp ‘ 𝐾 )
docaval.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
docaval.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
docaval.n 𝑁 = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
Assertion docafvalN ( ( 𝐾𝑉𝑊𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 docaval.j = ( join ‘ 𝐾 )
2 docaval.m = ( meet ‘ 𝐾 )
3 docaval.o = ( oc ‘ 𝐾 )
4 docaval.h 𝐻 = ( LHyp ‘ 𝐾 )
5 docaval.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 docaval.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
7 docaval.n 𝑁 = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
8 1 2 3 4 docaffvalN ( 𝐾𝑉 → ( ocA ‘ 𝐾 ) = ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) )
9 8 fveq1d ( 𝐾𝑉 → ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) ‘ 𝑊 ) )
10 7 9 syl5eq ( 𝐾𝑉𝑁 = ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) ‘ 𝑊 ) )
11 fveq2 ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 5 eqtr4di ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = 𝑇 )
13 12 pweqd ( 𝑤 = 𝑊 → 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = 𝒫 𝑇 )
14 fveq2 ( 𝑤 = 𝑊 → ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
15 14 6 eqtr4di ( 𝑤 = 𝑊 → ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) = 𝐼 )
16 15 cnveqd ( 𝑤 = 𝑊 ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) = 𝐼 )
17 15 rneqd ( 𝑤 = 𝑊 → ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) = ran 𝐼 )
18 17 rabeqdv ( 𝑤 = 𝑊 → { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } = { 𝑧 ∈ ran 𝐼𝑥𝑧 } )
19 18 inteqd ( 𝑤 = 𝑊 { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } = { 𝑧 ∈ ran 𝐼𝑥𝑧 } )
20 16 19 fveq12d ( 𝑤 = 𝑊 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) = ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) )
21 20 fveq2d ( 𝑤 = 𝑊 → ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) = ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) )
22 fveq2 ( 𝑤 = 𝑊 → ( 𝑤 ) = ( 𝑊 ) )
23 21 22 oveq12d ( 𝑤 = 𝑊 → ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) = ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) )
24 id ( 𝑤 = 𝑊𝑤 = 𝑊 )
25 23 24 oveq12d ( 𝑤 = 𝑊 → ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) = ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) )
26 15 25 fveq12d ( 𝑤 = 𝑊 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) = ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) )
27 13 26 mpteq12dv ( 𝑤 = 𝑊 → ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) ) )
28 eqid ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) = ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) )
29 5 fvexi 𝑇 ∈ V
30 29 pwex 𝒫 𝑇 ∈ V
31 30 mptex ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) ) ∈ V
32 27 28 31 fvmpt ( 𝑊𝐻 → ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ‘ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ∣ 𝑥𝑧 } ) ) ( 𝑤 ) ) 𝑤 ) ) ) ) ‘ 𝑊 ) = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) ) )
33 10 32 sylan9eq ( ( 𝐾𝑉𝑊𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑥𝑧 } ) ) ( 𝑊 ) ) 𝑊 ) ) ) )