dihvalrel

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

	Ref	Expression
Hypotheses	dihvalrel.h	$⊢ H = LHyp (K)$
	dihvalrel.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (X)$

Proof

Step	Hyp	Ref	Expression
1		dihvalrel.h	$⊢ H = LHyp (K)$
2		dihvalrel.i	$⊢ I = DIsoH (K) (W)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4	3 1 2	dihdm	$⊢ (K \in HL \land W \in H) \to dom I = {Base}_{K}$
5	4	eleq2d	$⊢ (K \in HL \land W \in H) \to (X \in dom I \leftrightarrow X \in {Base}_{K})$
6		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
7		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
8	3 1 2 6 7	dihss	$⊢ ((K \in HL \land W \in H) \land X \in {Base}_{K}) \to I (X) \subseteq {Base}_{DVecH (K) (W)}$
9		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
10		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
11	1 9 10 6 7	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{DVecH (K) (W)} = LTrn (K) (W) \times TEndo (K) (W)$
12	11	adantr	$⊢ ((K \in HL \land W \in H) \land X \in {Base}_{K}) \to {Base}_{DVecH (K) (W)} = LTrn (K) (W) \times TEndo (K) (W)$
13	8 12	sseqtrd	$⊢ ((K \in HL \land W \in H) \land X \in {Base}_{K}) \to I (X) \subseteq LTrn (K) (W) \times TEndo (K) (W)$
14		xpss	$⊢ LTrn (K) (W) \times TEndo (K) (W) \subseteq V \times V$
15	13 14	sstrdi	$⊢ ((K \in HL \land W \in H) \land X \in {Base}_{K}) \to I (X) \subseteq V \times V$
16		df-rel	$⊢ Rel I (X) \leftrightarrow I (X) \subseteq V \times V$
17	15 16	sylibr	$⊢ ((K \in HL \land W \in H) \land X \in {Base}_{K}) \to Rel I (X)$
18	17	ex	$⊢ (K \in HL \land W \in H) \to (X \in {Base}_{K} \to Rel I (X))$
19	5 18	sylbid	$⊢ (K \in HL \land W \in H) \to (X \in dom I \to Rel I (X))$
20		rel0	$⊢ Rel \emptyset$
21		ndmfv	$⊢ \neg X \in dom I \to I (X) = \emptyset$
22	21	releqd	$⊢ \neg X \in dom I \to (Rel I (X) \leftrightarrow Rel \emptyset)$
23	20 22	mpbiri	$⊢ \neg X \in dom I \to Rel I (X)$
24	19 23	pm2.61d1	$⊢ (K \in HL \land W \in H) \to Rel I (X)$

Metamath Proof Explorer

Theorem dihvalrel

Proof