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

Metamath Proof Explorer

Theorem dochval2

Proof