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

Metamath Proof Explorer

Theorem dochval2

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

Ref Expression
Hypotheses dochval2.o ⊢ ⊥ = ( oc ‘ 𝐾 )
dochval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochval2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochval2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochval2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochval2.n ⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochval2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) )

Proof

Step Hyp Ref Expression
1 dochval2.o ⊢ ⊥ = ( oc ‘ 𝐾 )
2 dochval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dochval2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dochval2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dochval2.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 dochval2.n ⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
9 7 8 1 2 3 4 5 6 dochval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) ) )
10 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
11 10 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝐾 ∈ CLat )
12 ssrab2 ⊢ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ⊆ ( Base ‘ 𝐾 )
13 7 8 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ⊆ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ∈ ( Base ‘ 𝐾 ) )
14 11 12 13 sylancl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ∈ ( Base ‘ 𝐾 ) )
15 7 2 3 dihcnvid1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) )
16 14 15 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) )
17 7 8 2 3 4 5 dihglb2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } )
18 17 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) ) = ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) )
19 16 18 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) = ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) )
20 19 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) = ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) )
21 20 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝐼 ‘ ( ⊥ ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑥 ) } ) ) ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) )
22 9 21 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( ◡ 𝐼 ‘ ∩ { 𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧 } ) ) ) )