mapdrvallem2

Description: Lemma for mapdrval . TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015)

	Ref	Expression
Hypotheses	mapdrval.h	$⊢ H = LHyp (K)$
	mapdrval.o	$⊢ O = ocH (K) (W)$
	mapdrval.m	$⊢ M = mapd (K) (W)$
	mapdrval.u	$⊢ U = DVecH (K) (W)$
	mapdrval.s	$⊢ S = LSubSp (U)$
	mapdrval.f	$⊢ F = LFnl (U)$
	mapdrval.l	$⊢ L = LKer (U)$
	mapdrval.d	$⊢ D = LDual (U)$
	mapdrval.t	$⊢ T = LSubSp (D)$
	mapdrval.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
	mapdrval.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdrval.r	$⊢ φ \to R \in T$
	mapdrval.e	$⊢ φ \to R \subseteq C$
	mapdrval.q	$⊢ Q = ⋃_{h \in R} O (L (h))$
	mapdrval.v	$⊢ V = {Base}_{U}$
	mapdrvallem2.a	$⊢ A = LSAtoms (U)$
	mapdrvallem2.n	$⊢ N = LSpan (U)$
	mapdrvallem2.z	$⊢ \underset{˙}{0} = 0_{U}$
	mapdrvallem2.y	$⊢ Y = 0_{D}$
Assertion	mapdrvallem2	$⊢ φ \to \{f \in C \| O (L (f)) \subseteq Q\} \subseteq R$

Proof

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		eleq1	$⊢ f = Y \to (f \in R \leftrightarrow Y \in R)$
21	11	3ad2ant1	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to (K \in HL \land W \in H)$
22	21	adantr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to (K \in HL \land W \in H)$
23		simpl2	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to f \in C$
24		simpr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to f \neq Y$
25		eldifsn	$⊢ f \in (C ∖ \{Y\}) \leftrightarrow (f \in C \land f \neq Y)$
26	23 24 25	sylanbrc	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to f \in (C ∖ \{Y\})$
27	1 2 4 15 17 18 6 7 8 19 10 22 26	lcfl8b	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to \exists x \in (V ∖ \{\underset{˙}{0}\}) O (L (f)) = N (\{x\})$
28		simp1l3	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to O (L (f)) \subseteq Q$
29		eqimss2	$⊢ O (L (f)) = N (\{x\}) \to N (\{x\}) \subseteq O (L (f))$
30	29	3ad2ant3	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to N (\{x\}) \subseteq O (L (f))$
31	1 4 11	dvhlmod	$⊢ φ \to U \in LMod$
32	31	3ad2ant1	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to U \in LMod$
33	32	adantr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to U \in LMod$
34	33	3ad2ant1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to U \in LMod$
35	22	3ad2ant1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to (K \in HL \land W \in H)$
36	10	lcfl1lem	$⊢ f \in C \leftrightarrow (f \in F \land O (O (L (f))) = L (f))$
37	36	simplbi	$⊢ f \in C \to f \in F$
38	37	3ad2ant2	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to f \in F$
39	38	adantr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to f \in F$
40	39	3ad2ant1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to f \in F$
41	15 6 7 34 40	lkrssv	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to L (f) \subseteq V$
42	1 4 15 5 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (f) \subseteq V) \to O (L (f)) \in S$
43	35 41 42	syl2anc	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to O (L (f)) \in S$
44		eldifi	$⊢ x \in (V ∖ \{\underset{˙}{0}\}) \to x \in V$
45	44	3ad2ant2	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to x \in V$
46	15 5 17 34 43 45	ellspsn5b	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to (x \in O (L (f)) \leftrightarrow N (\{x\}) \subseteq O (L (f)))$
47	30 46	mpbird	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to x \in O (L (f))$
48	28 47	sseldd	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to x \in Q$
49	48 14	eleqtrdi	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to x \in ⋃_{h \in R} O (L (h))$
50		eliun	$⊢ x \in ⋃_{h \in R} O (L (h)) \leftrightarrow \exists h \in R x \in O (L (h))$
51	49 50	sylib	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to \exists h \in R x \in O (L (h))$
52		eqid	$⊢ Scalar (U) = Scalar (U)$
53		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
54		eqid	$⊢ \cdot_{D} = \cdot_{D}$
55	1 4 11	dvhlvec	$⊢ φ \to U \in LVec$
56	55	3ad2ant1	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to U \in LVec$
57	56	adantr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to U \in LVec$
58	57	3ad2ant1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to U \in LVec$
59	58	ad2antrr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to U \in LVec$
60		simpr	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to h \in R$
61		simp1l1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to φ$
62	61	adantr	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to φ$
63	62 13	syl	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to R \subseteq C$
64	63	sseld	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to (h \in R \to h \in C)$
65	10	lcfl1lem	$⊢ h \in C \leftrightarrow (h \in F \land O (O (L (h))) = L (h))$
66	65	simplbi	$⊢ h \in C \to h \in F$
67	64 66	syl6	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to (h \in R \to h \in F)$
68	60 67	mpd	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to h \in F$
69	68	adantr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to h \in F$
70	40	ad2antrr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to f \in F$
71		simpll3	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to O (L (f)) = N (\{x\})$
72	34	ad2antrr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to U \in LMod$
73	35	ad2antrr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (K \in HL \land W \in H)$
74	15 6 7 72 69	lkrssv	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to L (h) \subseteq V$
75	1 4 15 5 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (h) \subseteq V) \to O (L (h)) \in S$
76	73 74 75	syl2anc	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to O (L (h)) \in S$
77		simpr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to x \in O (L (h))$
78	5 17 72 76 77	ellspsn5	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to N (\{x\}) \subseteq O (L (h))$
79		simpll2	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to x \in (V ∖ \{\underset{˙}{0}\})$
80	15 17 18 16 72 79	lsatlspsn	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to N (\{x\}) \in A$
81	1 2 4 18 16 6 7 73 69	dochsat0	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (O (L (h)) \in A \lor O (L (h)) = \{\underset{˙}{0}\})$
82	18 16 59 80 81	lsatcmp2	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (N (\{x\}) \subseteq O (L (h)) \leftrightarrow N (\{x\}) = O (L (h)))$
83	78 82	mpbid	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to N (\{x\}) = O (L (h))$
84	71 83	eqtr2d	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to O (L (h)) = O (L (f))$
85		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
86	61 13	syl	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to R \subseteq C$
87	86	sselda	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to h \in C$
88	87	adantr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to h \in C$
89	1 85 2 4 6 7 10 73 69	lcfl5	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (h \in C \leftrightarrow L (h) \in ran DIsoH (K) (W))$
90	88 89	mpbid	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to L (h) \in ran DIsoH (K) (W)$
91		simp1l2	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to f \in C$
92	91	ad2antrr	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to f \in C$
93	1 85 2 4 6 7 10 73 70	lcfl5	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (f \in C \leftrightarrow L (f) \in ran DIsoH (K) (W))$
94	92 93	mpbid	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to L (f) \in ran DIsoH (K) (W)$
95	1 85 2 73 90 94	doch11	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to (O (L (h)) = O (L (f)) \leftrightarrow L (h) = L (f))$
96	84 95	mpbid	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to L (h) = L (f)$
97	52 53 6 7 8 54 59 69 70 96	eqlkr4	$⊢ (((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \land x \in O (L (h))) \to \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h$
98	97	ex	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \land h \in R) \to (x \in O (L (h)) \to \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h)$
99	98	reximdva	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to (\exists h \in R x \in O (L (h)) \to \exists h \in R \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h)$
100	51 99	mpd	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to \exists h \in R \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h$
101		eleq1	$⊢ f = r \cdot_{D} h \to (f \in R \leftrightarrow r \cdot_{D} h \in R)$
102	101	reximi	$⊢ \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h \to \exists r \in {Base}_{Scalar (U)} (f \in R \leftrightarrow r \cdot_{D} h \in R)$
103	102	reximi	$⊢ \exists h \in R \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h \to \exists h \in R \exists r \in {Base}_{Scalar (U)} (f \in R \leftrightarrow r \cdot_{D} h \in R)$
104		rexcom	$⊢ \exists h \in R \exists r \in {Base}_{Scalar (U)} (f \in R \leftrightarrow r \cdot_{D} h \in R) \leftrightarrow \exists r \in {Base}_{Scalar (U)} \exists h \in R (f \in R \leftrightarrow r \cdot_{D} h \in R)$
105		df-rex	$⊢ \exists h \in R (f \in R \leftrightarrow r \cdot_{D} h \in R) \leftrightarrow \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))$
106	105	rexbii	$⊢ \exists r \in {Base}_{Scalar (U)} \exists h \in R (f \in R \leftrightarrow r \cdot_{D} h \in R) \leftrightarrow \exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))$
107	104 106	bitri	$⊢ \exists h \in R \exists r \in {Base}_{Scalar (U)} (f \in R \leftrightarrow r \cdot_{D} h \in R) \leftrightarrow \exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))$
108	103 107	sylib	$⊢ \exists h \in R \exists r \in {Base}_{Scalar (U)} f = r \cdot_{D} h \to \exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))$
109	100 108	syl	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to \exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))$
110	33	ad2antrr	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to U \in LMod$
111	12	3ad2ant1	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to R \in T$
112	111	adantr	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to R \in T$
113	112	ad2antrr	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to R \in T$
114		simplr	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to r \in {Base}_{Scalar (U)}$
115		simprl	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to h \in R$
116	52 53 8 54 9 110 113 114 115	ldualssvscl	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to r \cdot_{D} h \in R$
117		biimpr	$⊢ (f \in R \leftrightarrow r \cdot_{D} h \in R) \to (r \cdot_{D} h \in R \to f \in R)$
118	117	ad2antll	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to (r \cdot_{D} h \in R \to f \in R)$
119	116 118	mpd	$⊢ ((((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \land (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R))) \to f \in R$
120	119	ex	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \to ((h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R)) \to f \in R)$
121	120	exlimdv	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land r \in {Base}_{Scalar (U)}) \to (\exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R)) \to f \in R)$
122	121	rexlimdva	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to (\exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R)) \to f \in R)$
123	122	3ad2ant1	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to (\exists r \in {Base}_{Scalar (U)} \exists h (h \in R \land (f \in R \leftrightarrow r \cdot_{D} h \in R)) \to f \in R)$
124	109 123	mpd	$⊢ (((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \land x \in (V ∖ \{\underset{˙}{0}\}) \land O (L (f)) = N (\{x\})) \to f \in R$
125	124	rexlimdv3a	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to (\exists x \in (V ∖ \{\underset{˙}{0}\}) O (L (f)) = N (\{x\}) \to f \in R)$
126	27 125	mpd	$⊢ ((φ \land f \in C \land O (L (f)) \subseteq Q) \land f \neq Y) \to f \in R$
127	8 31	lduallmod	$⊢ φ \to D \in LMod$
128	127	3ad2ant1	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to D \in LMod$
129	19 9	lss0cl	$⊢ (D \in LMod \land R \in T) \to Y \in R$
130	128 111 129	syl2anc	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to Y \in R$
131	20 126 130	pm2.61ne	$⊢ (φ \land f \in C \land O (L (f)) \subseteq Q) \to f \in R$
132	131	rabssdv	$⊢ φ \to \{f \in C \| O (L (f)) \subseteq Q\} \subseteq R$

Metamath Proof Explorer

Theorem mapdrvallem2

Proof