This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochffval

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 ‘ 𝐾 )
Assertion dochffval ( 𝐾 ∈ 𝑉 → ( ocH ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dochval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dochval.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 dochval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
4 dochval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
7 6 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( DVecH ‘ 𝑘 ) = ( DVecH ‘ 𝐾 ) )
9 8 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) )
10 9 fveq2d ⊢ ( 𝑘 = 𝐾 → ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) )
11 10 pweqd ⊢ ( 𝑘 = 𝐾 → 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) )
12 fveq2 ⊢ ( 𝑘 = 𝐾 → ( DIsoH ‘ 𝑘 ) = ( DIsoH ‘ 𝐾 ) )
13 12 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) )
14 fveq2 ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ( oc ‘ 𝐾 ) )
15 14 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ⊥ )
16 fveq2 ⊢ ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = ( glb ‘ 𝐾 ) )
17 16 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = 𝐺 )
18 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
19 18 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
20 13 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) )
21 20 sseq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ↔ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) ) )
22 19 21 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } = { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } )
23 17 22 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) = ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) )
24 15 23 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) = ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) )
25 13 24 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) )
26 11 25 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) = ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) )
27 7 26 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )
28 df-doch ⊢ ocH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( oc ‘ 𝑘 ) ‘ ( ( glb ‘ 𝑘 ) ‘ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )
29 27 28 4 mptfvmpt ⊢ ( 𝐾 ∈ V → ( ocH ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )
30 5 29 syl ⊢ ( 𝐾 ∈ 𝑉 → ( ocH ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ 𝒫 ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑦 ) } ) ) ) ) ) )