Metamath Proof Explorer


Theorem doch2val2

Description: Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014)

Ref Expression
Hypotheses doch2val2.h 𝐻 = ( LHyp ‘ 𝐾 )
doch2val2.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
doch2val2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
doch2val2.v 𝑉 = ( Base ‘ 𝑈 )
doch2val2.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
doch2val2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
doch2val2.x ( 𝜑𝑋𝑉 )
Assertion doch2val2 ( 𝜑 → ( ‘ ( 𝑋 ) ) = { 𝑧 ∈ ran 𝐼𝑋𝑧 } )

Proof

Step Hyp Ref Expression
1 doch2val2.h 𝐻 = ( LHyp ‘ 𝐾 )
2 doch2val2.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 doch2val2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 doch2val2.v 𝑉 = ( Base ‘ 𝑈 )
5 doch2val2.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 doch2val2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 doch2val2.x ( 𝜑𝑋𝑉 )
8 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 8 1 2 3 4 5 dochval2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) )
10 6 7 9 syl2anc ( 𝜑 → ( 𝑋 ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) )
11 10 fveq2d ( 𝜑 → ( ‘ ( 𝑋 ) ) = ( ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) )
12 6 simpld ( 𝜑𝐾 ∈ HL )
13 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
14 12 13 syl ( 𝜑𝐾 ∈ OP )
15 ssrab2 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ⊆ ran 𝐼
16 15 a1i ( 𝜑 → { 𝑧 ∈ ran 𝐼𝑋𝑧 } ⊆ ran 𝐼 )
17 1 2 3 4 dih1rn ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑉 ∈ ran 𝐼 )
18 6 17 syl ( 𝜑𝑉 ∈ ran 𝐼 )
19 sseq2 ( 𝑧 = 𝑉 → ( 𝑋𝑧𝑋𝑉 ) )
20 19 elrab ( 𝑉 ∈ { 𝑧 ∈ ran 𝐼𝑋𝑧 } ↔ ( 𝑉 ∈ ran 𝐼𝑋𝑉 ) )
21 18 7 20 sylanbrc ( 𝜑𝑉 ∈ { 𝑧 ∈ ran 𝐼𝑋𝑧 } )
22 21 ne0d ( 𝜑 → { 𝑧 ∈ ran 𝐼𝑋𝑧 } ≠ ∅ )
23 1 2 dihintcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( { 𝑧 ∈ ran 𝐼𝑋𝑧 } ⊆ ran 𝐼 ∧ { 𝑧 ∈ ran 𝐼𝑋𝑧 } ≠ ∅ ) ) → { 𝑧 ∈ ran 𝐼𝑋𝑧 } ∈ ran 𝐼 )
24 6 16 22 23 syl12anc ( 𝜑 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ∈ ran 𝐼 )
25 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 25 1 2 dihcnvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { 𝑧 ∈ ran 𝐼𝑋𝑧 } ∈ ran 𝐼 ) → ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) )
27 6 24 26 syl2anc ( 𝜑 → ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) )
28 25 8 opoccl ( ( 𝐾 ∈ OP ∧ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) )
29 14 27 28 syl2anc ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) )
30 25 8 1 2 5 dochvalr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) )
31 6 29 30 syl2anc ( 𝜑 → ( ‘ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) )
32 25 8 opococ ( ( 𝐾 ∈ OP ∧ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) = ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) )
33 14 27 32 syl2anc ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) = ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) )
34 33 fveq2d ( 𝜑 → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) = ( 𝐼 ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) )
35 1 2 dihcnvid2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { 𝑧 ∈ ran 𝐼𝑋𝑧 } ∈ ran 𝐼 ) → ( 𝐼 ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) = { 𝑧 ∈ ran 𝐼𝑋𝑧 } )
36 6 24 35 syl2anc ( 𝜑 → ( 𝐼 ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) = { 𝑧 ∈ ran 𝐼𝑋𝑧 } )
37 34 36 eqtrd ( 𝜑 → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( 𝐼 { 𝑧 ∈ ran 𝐼𝑋𝑧 } ) ) ) ) = { 𝑧 ∈ ran 𝐼𝑋𝑧 } )
38 11 31 37 3eqtrd ( 𝜑 → ( ‘ ( 𝑋 ) ) = { 𝑧 ∈ ran 𝐼𝑋𝑧 } )