mapdrvallem3

Step	Hyp	Ref	Expression
1		mapdrval.h	$⊢ H = LHyp (K)$
2		mapdrval.o	$⊢ O = ocH (K) (W)$
3		mapdrval.m	$⊢ M = mapd (K) (W)$
4		mapdrval.u	$⊢ U = DVecH (K) (W)$
5		mapdrval.s	$⊢ S = LSubSp (U)$
6		mapdrval.f	$⊢ F = LFnl (U)$
7		mapdrval.l	$⊢ L = LKer (U)$
8		mapdrval.d	$⊢ D = LDual (U)$
9		mapdrval.t	$⊢ T = LSubSp (D)$
10		mapdrval.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
11		mapdrval.k	$⊢ φ \to (K \in HL \land W \in H)$
12		mapdrval.r	$⊢ φ \to R \in T$
13		mapdrval.e	$⊢ φ \to R \subseteq C$
14		mapdrval.q	$⊢ Q = ⋃_{h \in R} O (L (h))$
15		mapdrval.v	$⊢ V = {Base}_{U}$
16		mapdrvallem2.a	$⊢ A = LSAtoms (U)$
17		mapdrvallem2.n	$⊢ N = LSpan (U)$
18		mapdrvallem2.z	$⊢ \underset{˙}{0} = 0_{U}$
19		mapdrvallem2.y	$⊢ Y = 0_{D}$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	mapdrvallem2	$⊢ φ \to \{f \in C \| O (L (f)) \subseteq Q\} \subseteq R$
21		2fveq3	$⊢ h = f \to O (L (h)) = O (L (f))$
22	21	ssiun2s	$⊢ f \in R \to O (L (f)) \subseteq ⋃_{h \in R} O (L (h))$
23	22	adantl	$⊢ (φ \land f \in R) \to O (L (f)) \subseteq ⋃_{h \in R} O (L (h))$
24	23 14	sseqtrrdi	$⊢ (φ \land f \in R) \to O (L (f)) \subseteq Q$
25	13 24	ssrabdv	$⊢ φ \to R \subseteq \{f \in C \| O (L (f)) \subseteq Q\}$
26	20 25	eqssd	$⊢ φ \to \{f \in C \| O (L (f)) \subseteq Q\} = R$

Metamath Proof Explorer