Theorem dihvalrel

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

	Ref	Expression
Hypotheses	dihvalrel.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihvalrel.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dihvalrel	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		dihvalrel.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihvalrel.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4	3 1 2	dihdm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = ( Base ‘ 𝐾 ) )
5	4	eleq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ ( Base ‘ 𝐾 ) ) )
6		eqid	⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		eqid	⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
8	3 1 2 6 7	dihss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
9		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11	1 9 10 6 7	dvhvbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
12	11	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
13	8 12	sseqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
14		xpss	⊢ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ⊆ ( V × V )
15	13 14	sstrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( V × V ) )
16		df-rel	⊢ ( Rel ( 𝐼 ‘ 𝑋 ) ↔ ( 𝐼 ‘ 𝑋 ) ⊆ ( V × V ) )
17	15 16	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → Rel ( 𝐼 ‘ 𝑋 ) )
18	17	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ ( Base ‘ 𝐾 ) → Rel ( 𝐼 ‘ 𝑋 ) ) )
19	5 18	sylbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) ) )
20		rel0	⊢ Rel ∅
21		ndmfv	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ )
22	21	releqd	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) )
23	20 22	mpbiri	⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) )
24	19 23	pm2.61d1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )