Theorem dihlss

Description: The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014)

	Ref	Expression
Hypotheses	dihlss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihlss.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion	dihlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dihlss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dihlss.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dihlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dihlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7		eqid	⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8	1 6 2 3 7	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) )
9	1 6 2 4 7 5	diblss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ 𝑆 )
10	8 9	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )
11	10	anassrs	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )
12		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
13		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
14		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
15		eqid	⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
16		eqid	⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
17	1 6 12 13 14 2 3 7 15 4 5 16	dihlsscpre	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )
18	17	anassrs	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )
19	11 18	pm2.61dan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )