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 ⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) )