Theorem dochval

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

	Ref	Expression
Hypotheses	dochval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dochval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	dochval.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	dochval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochval.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dochval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochval.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dochval	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dochval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
3		dochval.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4		dochval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dochval.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6		dochval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		dochval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
8		dochval.n	⊢ 𝑁 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9	1 2 3 4 5 6 7 8	dochfval	⊢ ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) )
10	9	adantr	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑁 = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) )
11	10	fveq1d	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) ‘ 𝑋 ) )
12	7	fvexi	⊢ 𝑉 ∈ V
13	12	elpw2	⊢ ( 𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉 )
14	13	biimpri	⊢ ( 𝑋 ⊆ 𝑉 → 𝑋 ∈ 𝒫 𝑉 )
15	14	adantl	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ∈ 𝒫 𝑉 )
16		fvex	⊢ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ∈ V
17		sseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) ↔ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) ) )
18	17	rabbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } = { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } )
19	18	fveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) = ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) )
20	19	fveq2d	⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) = ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) )
21	20	fveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) = ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
22		eqid	⊢ ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) = ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
23	21 22	fvmptg	⊢ ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ∈ V ) → ( ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
24	15 16 23	sylancl	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ( 𝑥 ∈ 𝒫 𝑉 ↦ ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) ) ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )
25	11 24	eqtrd	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( 𝐼 ‘ ( ⊥ ‘ ( 𝐺 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ ( 𝐼 ‘ 𝑦 ) } ) ) ) )