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 𝐼 ∣ 𝑋 ⊆ 𝑧 } )