Metamath Proof Explorer

Theorem docavalN

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 docavalN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ 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 5 6 7 docafvalN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) )
10 9 fveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) ‘ 𝑋 ) )
11 5 fvexi ⊢ 𝑇 ∈ V
12 11 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝑇 ↔ 𝑋 ⊆ 𝑇 )
13 12 biimpri ⊢ ( 𝑋 ⊆ 𝑇 → 𝑋 ∈ 𝒫 𝑇 )
14 13 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → 𝑋 ∈ 𝒫 𝑇 )
15 fvex ⊢ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ∈ V
16 sseq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑧 ) )
17 16 rabbidv ⊢ ( 𝑥 = 𝑋 → { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } = { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } )
18 17 inteqd ⊢ ( 𝑥 = 𝑋 → ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } )
19 18 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) = ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) )
20 19 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) = ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) = ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) )
22 21 fvoveq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) = ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) )
23 eqid ⊢ ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) = ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) )
24 22 23 fvmptg ⊢ ( ( 𝑋 ∈ 𝒫 𝑇 ∧ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ∈ V ) → ( ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) ‘ 𝑋 ) = ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) )
25 14 15 24 sylancl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( ( 𝑥 ∈ 𝒫 𝑇 ↦ ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) ) ‘ 𝑋 ) = ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) )
26 10 25 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ( ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ∨ ( ⊥ ‘ 𝑊 ) ) ∧ 𝑊 ) ) )