dih1dimatlem

	Ref	Expression
Hypotheses	dih1dimat.h	$⊢ H = LHyp (K)$
	dih1dimat.u	$⊢ U = DVecH (K) (W)$
	dih1dimat.i	$⊢ I = DIsoH (K) (W)$
	dih1dimat.a	$⊢ A = LSAtoms (U)$
	dih1dimat.b	$⊢ B = {Base}_{K}$
	dih1dimat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dih1dimat.c	$⊢ C = Atoms (K)$
	dih1dimat.p	$⊢ P = oc (K) (W)$
	dih1dimat.t	$⊢ T = LTrn (K) (W)$
	dih1dimat.r	$⊢ R = trL (K) (W)$
	dih1dimat.e	$⊢ E = TEndo (K) (W)$
	dih1dimat.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dih1dimat.d	$⊢ F = Scalar (U)$
	dih1dimat.j	$⊢ J = {inv}_{r} (F)$
	dih1dimat.v	$⊢ V = {Base}_{U}$
	dih1dimat.m	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	dih1dimat.s	$⊢ S = LSubSp (U)$
	dih1dimat.n	$⊢ N = LSpan (U)$
	dih1dimat.z	$⊢ \underset{˙}{0} = 0_{U}$
	dih1dimat.g	$⊢ G = (ι h \in T \| h (P) = J (s) (f) (P))$
Assertion	dih1dimatlem	$⊢ ((K \in HL \land W \in H) \land D \in A) \to D \in ran I$

Proof

Step	Hyp	Ref	Expression
1		dih1dimat.h	$⊢ H = LHyp (K)$
2		dih1dimat.u	$⊢ U = DVecH (K) (W)$
3		dih1dimat.i	$⊢ I = DIsoH (K) (W)$
4		dih1dimat.a	$⊢ A = LSAtoms (U)$
5		dih1dimat.b	$⊢ B = {Base}_{K}$
6		dih1dimat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
7		dih1dimat.c	$⊢ C = Atoms (K)$
8		dih1dimat.p	$⊢ P = oc (K) (W)$
9		dih1dimat.t	$⊢ T = LTrn (K) (W)$
10		dih1dimat.r	$⊢ R = trL (K) (W)$
11		dih1dimat.e	$⊢ E = TEndo (K) (W)$
12		dih1dimat.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
13		dih1dimat.d	$⊢ F = Scalar (U)$
14		dih1dimat.j	$⊢ J = {inv}_{r} (F)$
15		dih1dimat.v	$⊢ V = {Base}_{U}$
16		dih1dimat.m	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
17		dih1dimat.s	$⊢ S = LSubSp (U)$
18		dih1dimat.n	$⊢ N = LSpan (U)$
19		dih1dimat.z	$⊢ \underset{˙}{0} = 0_{U}$
20		dih1dimat.g	$⊢ G = (ι h \in T \| h (P) = J (s) (f) (P))$
21		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
22	1 2 21	dvhlvec	$⊢ (K \in HL \land W \in H) \to U \in LVec$
23	15 18 19 4	islsat	$⊢ U \in LVec \to (D \in A \leftrightarrow \exists v \in (V ∖ \{\underset{˙}{0}\}) D = N (\{v\}))$
24	22 23	syl	$⊢ (K \in HL \land W \in H) \to (D \in A \leftrightarrow \exists v \in (V ∖ \{\underset{˙}{0}\}) D = N (\{v\}))$
25	24	biimpa	$⊢ ((K \in HL \land W \in H) \land D \in A) \to \exists v \in (V ∖ \{\underset{˙}{0}\}) D = N (\{v\})$
26		eldifi	$⊢ v \in (V ∖ \{\underset{˙}{0}\}) \to v \in V$
27	1 9 11 2 15	dvhvbase	$⊢ (K \in HL \land W \in H) \to V = T \times E$
28	27	eleq2d	$⊢ (K \in HL \land W \in H) \to (v \in V \leftrightarrow v \in (T \times E))$
29	26 28	syl5ib	$⊢ (K \in HL \land W \in H) \to (v \in (V ∖ \{\underset{˙}{0}\}) \to v \in (T \times E))$
30	29	imp	$⊢ ((K \in HL \land W \in H) \land v \in (V ∖ \{\underset{˙}{0}\})) \to v \in (T \times E)$
31		simpr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to s = O$
32	31	opeq2d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to ⟨f, s⟩ = ⟨f, O⟩$
33	32	sneqd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to \{⟨f, s⟩\} = \{⟨f, O⟩\}$
34	33	fveq2d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to N (\{⟨f, s⟩\}) = N (\{⟨f, O⟩\})$
35		simpl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to (K \in HL \land W \in H)$
36	5 1 9 10	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \in B$
37	6 1 9 10	trlle	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \underset{˙}{\leq} W$
38		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
39	5 6 1 3 38	dihvalb	$⊢ ((K \in HL \land W \in H) \land (R (f) \in B \land R (f) \underset{˙}{\leq} W)) \to I (R (f)) = DIsoB (K) (W) (R (f))$
40	35 36 37 39	syl12anc	$⊢ ((K \in HL \land W \in H) \land f \in T) \to I (R (f)) = DIsoB (K) (W) (R (f))$
41	5 1 9 10 12 2 38 18	dib1dim2	$⊢ ((K \in HL \land W \in H) \land f \in T) \to DIsoB (K) (W) (R (f)) = N (\{⟨f, O⟩\})$
42	40 41	eqtr2d	$⊢ ((K \in HL \land W \in H) \land f \in T) \to N (\{⟨f, O⟩\}) = I (R (f))$
43	5 1 3 2 17	dihf11	$⊢ (K \in HL \land W \in H) \to I : B \underset{1-1}{⟶} S$
44	43	adantr	$⊢ ((K \in HL \land W \in H) \land f \in T) \to I : B \underset{1-1}{⟶} S$
45		f1fn	$⊢ I : B \underset{1-1}{⟶} S \to I Fn B$
46	44 45	syl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to I Fn B$
47		fnfvelrn	$⊢ (I Fn B \land R (f) \in B) \to I (R (f)) \in ran I$
48	46 36 47	syl2anc	$⊢ ((K \in HL \land W \in H) \land f \in T) \to I (R (f)) \in ran I$
49	42 48	eqeltrd	$⊢ ((K \in HL \land W \in H) \land f \in T) \to N (\{⟨f, O⟩\}) \in ran I$
50	49	adantrr	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E)) \to N (\{⟨f, O⟩\}) \in ran I$
51	50	adantr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to N (\{⟨f, O⟩\}) \in ran I$
52	34 51	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s = O) \to N (\{⟨f, s⟩\}) \in ran I$
53		simpll	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (K \in HL \land W \in H)$
54		eqid	$⊢ {Base}_{F} = {Base}_{F}$
55	1 11 2 13 54	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{F} = E$
56	53 55	syl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to {Base}_{F} = E$
57	56	rexeqdv	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (\exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩ \leftrightarrow \exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩)$
58		simplll	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to (K \in HL \land W \in H)$
59		simpr	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to t \in E$
60		opelxpi	$⊢ (f \in T \land s \in E) \to ⟨f, s⟩ \in (T \times E)$
61	60	ad3antlr	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to ⟨f, s⟩ \in (T \times E)$
62	1 9 11 2 16	dvhvscacl	$⊢ ((K \in HL \land W \in H) \land (t \in E \land ⟨f, s⟩ \in (T \times E))) \to t \underset{˙}{\cdot} ⟨f, s⟩ \in (T \times E)$
63	58 59 61 62	syl12anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to t \underset{˙}{\cdot} ⟨f, s⟩ \in (T \times E)$
64		eleq1a	$⊢ t \underset{˙}{\cdot} ⟨f, s⟩ \in (T \times E) \to (u = t \underset{˙}{\cdot} ⟨f, s⟩ \to u \in (T \times E))$
65	63 64	syl	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to (u = t \underset{˙}{\cdot} ⟨f, s⟩ \to u \in (T \times E))$
66	65	rexlimdva	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (\exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩ \to u \in (T \times E))$
67	66	pm4.71rd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (\exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩ \leftrightarrow (u \in (T \times E) \land \exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩))$
68		simplrl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to f \in T$
69	68	adantr	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to f \in T$
70		simplrr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to s \in E$
71	70	adantr	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to s \in E$
72	1 9 11 2 16	dvhopvsca	$⊢ ((K \in HL \land W \in H) \land (t \in E \land f \in T \land s \in E)) \to t \underset{˙}{\cdot} ⟨f, s⟩ = ⟨t (f), t \circ s⟩$
73	58 59 69 71 72	syl13anc	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to t \underset{˙}{\cdot} ⟨f, s⟩ = ⟨t (f), t \circ s⟩$
74	73	eqeq2d	$⊢ ((((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \land t \in E) \to (u = t \underset{˙}{\cdot} ⟨f, s⟩ \leftrightarrow u = ⟨t (f), t \circ s⟩)$
75	74	rexbidva	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (\exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩ \leftrightarrow \exists t \in E u = ⟨t (f), t \circ s⟩)$
76	75	anbi2d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to ((u \in (T \times E) \land \exists t \in E u = t \underset{˙}{\cdot} ⟨f, s⟩) \leftrightarrow (u \in (T \times E) \land \exists t \in E u = ⟨t (f), t \circ s⟩))$
77	57 67 76	3bitrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (\exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩ \leftrightarrow (u \in (T \times E) \land \exists t \in E u = ⟨t (f), t \circ s⟩))$
78	77	abbidv	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to \{u \| \exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩\} = \{u \| (u \in (T \times E) \land \exists t \in E u = ⟨t (f), t \circ s⟩)\}$
79		df-rab	$⊢ \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} = \{u \| (u \in (T \times E) \land \exists t \in E u = ⟨t (f), t \circ s⟩)\}$
80	78 79	eqtr4di	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to \{u \| \exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩\} = \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\}$
81		ssrab2	$⊢ \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} \subseteq T \times E$
82		relxp	$⊢ Rel (T \times E)$
83		relss	$⊢ \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} \subseteq T \times E \to (Rel (T \times E) \to Rel \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\})$
84	81 82 83	mp2	$⊢ Rel \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\}$
85		relopab	$⊢ Rel \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
86		vex	$⊢ i \in V$
87		vex	$⊢ p \in V$
88		eqeq1	$⊢ g = i \to (g = r (G) \leftrightarrow i = r (G))$
89	88	anbi1d	$⊢ g = i \to ((g = r (G) \land r \in E) \leftrightarrow (i = r (G) \land r \in E))$
90		fveq1	$⊢ r = p \to r (G) = p (G)$
91	90	eqeq2d	$⊢ r = p \to (i = r (G) \leftrightarrow i = p (G))$
92		eleq1w	$⊢ r = p \to (r \in E \leftrightarrow p \in E)$
93	91 92	anbi12d	$⊢ r = p \to ((i = r (G) \land r \in E) \leftrightarrow (i = p (G) \land p \in E))$
94	86 87 89 93	opelopab	$⊢ ⟨i, p⟩ \in \{⟨g, r⟩ \| (g = r (G) \land r \in E)\} \leftrightarrow (i = p (G) \land p \in E)$
95	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	dih1dimatlem0	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s)))$
96	95	3expa	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s)))$
97		opelxp	$⊢ ⟨i, p⟩ \in (T \times E) \leftrightarrow (i \in T \land p \in E)$
98	86 87	opth	$⊢ ⟨i, p⟩ = ⟨t (f), t \circ s⟩ \leftrightarrow (i = t (f) \land p = t \circ s)$
99	98	rexbii	$⊢ \exists t \in E ⟨i, p⟩ = ⟨t (f), t \circ s⟩ \leftrightarrow \exists t \in E (i = t (f) \land p = t \circ s)$
100	97 99	anbi12i	$⊢ (⟨i, p⟩ \in (T \times E) \land \exists t \in E ⟨i, p⟩ = ⟨t (f), t \circ s⟩) \leftrightarrow ((i \in T \land p \in E) \land \exists t \in E (i = t (f) \land p = t \circ s))$
101	96 100	syl6bbr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow (⟨i, p⟩ \in (T \times E) \land \exists t \in E ⟨i, p⟩ = ⟨t (f), t \circ s⟩))$
102		eqeq1	$⊢ u = ⟨i, p⟩ \to (u = ⟨t (f), t \circ s⟩ \leftrightarrow ⟨i, p⟩ = ⟨t (f), t \circ s⟩)$
103	102	rexbidv	$⊢ u = ⟨i, p⟩ \to (\exists t \in E u = ⟨t (f), t \circ s⟩ \leftrightarrow \exists t \in E ⟨i, p⟩ = ⟨t (f), t \circ s⟩)$
104	103	elrab	$⊢ ⟨i, p⟩ \in \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} \leftrightarrow (⟨i, p⟩ \in (T \times E) \land \exists t \in E ⟨i, p⟩ = ⟨t (f), t \circ s⟩)$
105	101 104	syl6bbr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to ((i = p (G) \land p \in E) \leftrightarrow ⟨i, p⟩ \in \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\})$
106	94 105	syl5rbb	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (⟨i, p⟩ \in \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} \leftrightarrow ⟨i, p⟩ \in \{⟨g, r⟩ \| (g = r (G) \land r \in E)\})$
107	84 85 106	eqrelrdv	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to \{u \in (T \times E) \| \exists t \in E u = ⟨t (f), t \circ s⟩\} = \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
108	80 107	eqtrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to \{u \| \exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩\} = \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
109	1 2 53	dvhlmod	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to U \in LMod$
110	1 9 11 2 15	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E)) \to ⟨f, s⟩ \in V$
111	110	adantr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to ⟨f, s⟩ \in V$
112	13 54 15 16 18	lspsn	$⊢ (U \in LMod \land ⟨f, s⟩ \in V) \to N (\{⟨f, s⟩\}) = \{u \| \exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩\}$
113	109 111 112	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to N (\{⟨f, s⟩\}) = \{u \| \exists t \in {Base}_{F} u = t \underset{˙}{\cdot} ⟨f, s⟩\}$
114		simpr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to s \neq O$
115	5 1 9 11 12 2 13 14	tendoinvcl	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to (J (s) \in E \land J (s) \neq O)$
116	115	simpld	$⊢ ((K \in HL \land W \in H) \land s \in E \land s \neq O) \to J (s) \in E$
117	53 70 114 116	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to J (s) \in E$
118	1 9 11	tendocl	$⊢ ((K \in HL \land W \in H) \land J (s) \in E \land f \in T) \to J (s) (f) \in T$
119	53 117 68 118	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to J (s) (f) \in T$
120	6 7 1 8	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in C \land \neg P \underset{˙}{\leq} W)$
121	53 120	syl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (P \in C \land \neg P \underset{˙}{\leq} W)$
122	6 7 1 9	ltrnel	$⊢ ((K \in HL \land W \in H) \land J (s) (f) \in T \land (P \in C \land \neg P \underset{˙}{\leq} W)) \to (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)$
123	53 119 121 122	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)$
124		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
125	6 7 1 124 3	dihvalcqat	$⊢ ((K \in HL \land W \in H) \land (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)) \to I (J (s) (f) (P)) = DIsoC (K) (W) (J (s) (f) (P))$
126	53 123 125	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to I (J (s) (f) (P)) = DIsoC (K) (W) (J (s) (f) (P))$
127	6 7 1 8 9 11 124 20	dicval2	$⊢ ((K \in HL \land W \in H) \land (J (s) (f) (P) \in C \land \neg J (s) (f) (P) \underset{˙}{\leq} W)) \to DIsoC (K) (W) (J (s) (f) (P)) = \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
128	53 123 127	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to DIsoC (K) (W) (J (s) (f) (P)) = \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
129	126 128	eqtrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to I (J (s) (f) (P)) = \{⟨g, r⟩ \| (g = r (G) \land r \in E)\}$
130	108 113 129	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to N (\{⟨f, s⟩\}) = I (J (s) (f) (P))$
131	5 1 3	dihfn	$⊢ (K \in HL \land W \in H) \to I Fn B$
132	131	adantr	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E)) \to I Fn B$
133	132	adantr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to I Fn B$
134		simplll	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to K \in HL$
135		hlop	$⊢ K \in HL \to K \in OP$
136	134 135	syl	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to K \in OP$
137	5 1	lhpbase	$⊢ W \in H \to W \in B$
138	137	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to W \in B$
139		eqid	$⊢ oc (K) = oc (K)$
140	5 139	opoccl	$⊢ (K \in OP \land W \in B) \to oc (K) (W) \in B$
141	136 138 140	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to oc (K) (W) \in B$
142	8 141	eqeltrid	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to P \in B$
143	5 1 9	ltrncl	$⊢ ((K \in HL \land W \in H) \land J (s) (f) \in T \land P \in B) \to J (s) (f) (P) \in B$
144	53 119 142 143	syl3anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to J (s) (f) (P) \in B$
145		fnfvelrn	$⊢ (I Fn B \land J (s) (f) (P) \in B) \to I (J (s) (f) (P)) \in ran I$
146	133 144 145	syl2anc	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to I (J (s) (f) (P)) \in ran I$
147	130 146	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (f \in T \land s \in E)) \land s \neq O) \to N (\{⟨f, s⟩\}) \in ran I$
148	52 147	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land (f \in T \land s \in E)) \to N (\{⟨f, s⟩\}) \in ran I$
149	148	ralrimivva	$⊢ (K \in HL \land W \in H) \to \forall f \in T \forall s \in E N (\{⟨f, s⟩\}) \in ran I$
150		sneq	$⊢ v = ⟨f, s⟩ \to \{v\} = \{⟨f, s⟩\}$
151	150	fveq2d	$⊢ v = ⟨f, s⟩ \to N (\{v\}) = N (\{⟨f, s⟩\})$
152	151	eleq1d	$⊢ v = ⟨f, s⟩ \to (N (\{v\}) \in ran I \leftrightarrow N (\{⟨f, s⟩\}) \in ran I)$
153	152	ralxp	$⊢ \forall v \in (T \times E) N (\{v\}) \in ran I \leftrightarrow \forall f \in T \forall s \in E N (\{⟨f, s⟩\}) \in ran I$
154	149 153	sylibr	$⊢ (K \in HL \land W \in H) \to \forall v \in (T \times E) N (\{v\}) \in ran I$
155	154	r19.21bi	$⊢ ((K \in HL \land W \in H) \land v \in (T \times E)) \to N (\{v\}) \in ran I$
156	30 155	syldan	$⊢ ((K \in HL \land W \in H) \land v \in (V ∖ \{\underset{˙}{0}\})) \to N (\{v\}) \in ran I$
157		eleq1a	$⊢ N (\{v\}) \in ran I \to (D = N (\{v\}) \to D \in ran I)$
158	156 157	syl	$⊢ ((K \in HL \land W \in H) \land v \in (V ∖ \{\underset{˙}{0}\})) \to (D = N (\{v\}) \to D \in ran I)$
159	158	rexlimdva	$⊢ (K \in HL \land W \in H) \to (\exists v \in (V ∖ \{\underset{˙}{0}\}) D = N (\{v\}) \to D \in ran I)$
160	159	adantr	$⊢ ((K \in HL \land W \in H) \land D \in A) \to (\exists v \in (V ∖ \{\underset{˙}{0}\}) D = N (\{v\}) \to D \in ran I)$
161	25 160	mpd	$⊢ ((K \in HL \land W \in H) \land D \in A) \to D \in ran I$

Metamath Proof Explorer

Theorem dih1dimatlem

Proof