Metamath Proof Explorer


Theorem dochfval

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochval.b 𝐵 = ( Base ‘ 𝐾 )
dochval.g 𝐺 = ( glb ‘ 𝐾 )
dochval.o = ( oc ‘ 𝐾 )
dochval.h 𝐻 = ( LHyp ‘ 𝐾 )
dochval.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochval.v 𝑉 = ( Base ‘ 𝑈 )
dochval.n 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochfval ( ( 𝐾𝑋𝑊𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dochval.b 𝐵 = ( Base ‘ 𝐾 )
2 dochval.g 𝐺 = ( glb ‘ 𝐾 )
3 dochval.o = ( oc ‘ 𝐾 )
4 dochval.h 𝐻 = ( LHyp ‘ 𝐾 )
5 dochval.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dochval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 dochval.v 𝑉 = ( Base ‘ 𝑈 )
8 dochval.n 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9 1 2 3 4 dochffval ( 𝐾𝑋 → ( ocH ‘ 𝐾 ) = ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )
10 9 fveq1d ( 𝐾𝑋 → ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) ‘ 𝑊 ) )
11 8 10 syl5eq ( 𝐾𝑋𝑁 = ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) ‘ 𝑊 ) )
12 fveq2 ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
13 12 6 eqtr4di ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑈 )
14 13 fveq2d ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( Base ‘ 𝑈 ) )
15 14 7 eqtr4di ( 𝑤 = 𝑊 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑉 )
16 15 pweqd ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝒫 𝑉 )
17 fveq2 ( 𝑤 = 𝑊 → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
18 17 5 eqtr4di ( 𝑤 = 𝑊 → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) = 𝐼 )
19 18 fveq1d ( 𝑤 = 𝑊 → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) = ( 𝐼𝑦 ) )
20 19 sseq2d ( 𝑤 = 𝑊 → ( 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ↔ 𝑥 ⊆ ( 𝐼𝑦 ) ) )
21 20 rabbidv ( 𝑤 = 𝑊 → { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } = { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } )
22 21 fveq2d ( 𝑤 = 𝑊 → ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) = ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) )
23 22 fveq2d ( 𝑤 = 𝑊 → ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) = ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) )
24 18 23 fveq12d ( 𝑤 = 𝑊 → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) = ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) )
25 16 24 mpteq12dv ( 𝑤 = 𝑊 → ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )
26 eqid ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) = ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) )
27 7 fvexi 𝑉 ∈ V
28 27 pwex 𝒫 𝑉 ∈ V
29 28 mptex ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) ∈ V
30 25 26 29 fvmpt ( 𝑊𝐻 → ( ( 𝑤𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) ‘ 𝑊 ) = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )
31 11 30 sylan9eq ( ( 𝐾𝑋𝑊𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ‘ ( 𝐺 ‘ { 𝑦𝐵𝑥 ⊆ ( 𝐼𝑦 ) } ) ) ) ) )