mapdordlem2

Description: Lemma for mapdord . Ordering property of projectivity M . TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the T hypothesis. (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	mapdord.h	$⊢ H = LHyp (K)$
	mapdord.u	$⊢ U = DVecH (K) (W)$
	mapdord.s	$⊢ S = LSubSp (U)$
	mapdord.m	$⊢ M = mapd (K) (W)$
	mapdord.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdord.x	$⊢ φ \to X \in S$
	mapdord.y	$⊢ φ \to Y \in S$
	mapdord.o	$⊢ O = ocH (K) (W)$
	mapdord.a	$⊢ A = LSAtoms (U)$
	mapdord.f	$⊢ F = LFnl (U)$
	mapdord.c	$⊢ J = LSHyp (U)$
	mapdord.l	$⊢ L = LKer (U)$
	mapdord.t	$⊢ T = \{g \in F \| O (O (L (g))) \in J\}$
	mapdord.q	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
Assertion	mapdordlem2	$⊢ φ \to (M (X) \subseteq M (Y) \leftrightarrow X \subseteq Y)$

Proof

Step	Hyp	Ref	Expression
1		mapdord.h	$⊢ H = LHyp (K)$
2		mapdord.u	$⊢ U = DVecH (K) (W)$
3		mapdord.s	$⊢ S = LSubSp (U)$
4		mapdord.m	$⊢ M = mapd (K) (W)$
5		mapdord.k	$⊢ φ \to (K \in HL \land W \in H)$
6		mapdord.x	$⊢ φ \to X \in S$
7		mapdord.y	$⊢ φ \to Y \in S$
8		mapdord.o	$⊢ O = ocH (K) (W)$
9		mapdord.a	$⊢ A = LSAtoms (U)$
10		mapdord.f	$⊢ F = LFnl (U)$
11		mapdord.c	$⊢ J = LSHyp (U)$
12		mapdord.l	$⊢ L = LKer (U)$
13		mapdord.t	$⊢ T = \{g \in F \| O (O (L (g))) \in J\}$
14		mapdord.q	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
15	1 2 3 10 12 8 4 5 6 14	mapdvalc	$⊢ φ \to M (X) = \{f \in C \| O (L (f)) \subseteq X\}$
16	1 2 3 10 12 8 4 5 7 14	mapdvalc	$⊢ φ \to M (Y) = \{f \in C \| O (L (f)) \subseteq Y\}$
17	15 16	sseq12d	$⊢ φ \to (M (X) \subseteq M (Y) \leftrightarrow \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\})$
18		ss2rab	$⊢ \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \leftrightarrow \forall f \in C (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)$
19		eqid	$⊢ {Base}_{U} = {Base}_{U}$
20	1 8 2 19 11 10 12 13 14 5	mapdordlem1a	$⊢ φ \to (f \in T \leftrightarrow (f \in C \land O (O (L (f))) \in J))$
21		simprl	$⊢ (φ \land (f \in C \land O (O (L (f))) \in J)) \to f \in C$
22		idd	$⊢ (φ \land (f \in C \land O (O (L (f))) \in J)) \to ((O (L (f)) \subseteq X \to O (L (f)) \subseteq Y) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
23	21 22	embantd	$⊢ (φ \land (f \in C \land O (O (L (f))) \in J)) \to ((f \in C \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
24	23	ex	$⊢ φ \to ((f \in C \land O (O (L (f))) \in J) \to ((f \in C \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)))$
25	20 24	sylbid	$⊢ φ \to (f \in T \to ((f \in C \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)))$
26	25	com23	$⊢ φ \to ((f \in C \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)) \to (f \in T \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)))$
27	26	ralimdv2	$⊢ φ \to (\forall f \in C (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y) \to \forall f \in T (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
28	18 27	biimtrid	$⊢ φ \to (\{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \to \forall f \in T (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
29	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
30	3 9 29 6 7	lssatle	$⊢ φ \to (X \subseteq Y \leftrightarrow \forall p \in A (p \subseteq X \to p \subseteq Y))$
31	13	mapdordlem1	$⊢ f \in T \leftrightarrow (f \in F \land O (O (L (f))) \in J)$
32	31	simprbi	$⊢ f \in T \to O (O (L (f))) \in J$
33	32	adantl	$⊢ (φ \land f \in T) \to O (O (L (f))) \in J$
34	5	adantr	$⊢ (φ \land f \in T) \to (K \in HL \land W \in H)$
35	31	simplbi	$⊢ f \in T \to f \in F$
36	35	adantl	$⊢ (φ \land f \in T) \to f \in F$
37	1 8 2 10 11 12 34 36	dochlkr	$⊢ (φ \land f \in T) \to (O (O (L (f))) \in J \leftrightarrow (O (O (L (f))) = L (f) \land L (f) \in J))$
38	33 37	mpbid	$⊢ (φ \land f \in T) \to (O (O (L (f))) = L (f) \land L (f) \in J)$
39	38	simpld	$⊢ (φ \land f \in T) \to O (O (L (f))) = L (f)$
40	38	simprd	$⊢ (φ \land f \in T) \to L (f) \in J$
41	1 8 2 9 11 34 40	dochshpsat	$⊢ (φ \land f \in T) \to (O (O (L (f))) = L (f) \leftrightarrow O (L (f)) \in A)$
42	39 41	mpbid	$⊢ (φ \land f \in T) \to O (L (f)) \in A$
43	1 2 5	dvhlvec	$⊢ φ \to U \in LVec$
44	5	adantr	$⊢ (φ \land p \in A) \to (K \in HL \land W \in H)$
45		simpr	$⊢ (φ \land p \in A) \to p \in A$
46	1 2 8 9 11 44 45	dochsatshp	$⊢ (φ \land p \in A) \to O (p) \in J$
47	11 10 12	lshpkrex	$⊢ (U \in LVec \land O (p) \in J) \to \exists f \in F L (f) = O (p)$
48	43 46 47	syl2an2r	$⊢ (φ \land p \in A) \to \exists f \in F L (f) = O (p)$
49		simprl	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to f \in F$
50		simprr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to L (f) = O (p)$
51	50	fveq2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (L (f)) = O (O (p))$
52	51	fveq2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) = O (O (O (p)))$
53	29	adantr	$⊢ (φ \land p \in A) \to U \in LMod$
54	19 9 53 45	lsatssv	$⊢ (φ \land p \in A) \to p \subseteq {Base}_{U}$
55		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
56	1 55 2 19 8	dochcl	$⊢ ((K \in HL \land W \in H) \land p \subseteq {Base}_{U}) \to O (p) \in ran DIsoH (K) (W)$
57	5 54 56	syl2an2r	$⊢ (φ \land p \in A) \to O (p) \in ran DIsoH (K) (W)$
58	1 55 8	dochoc	$⊢ ((K \in HL \land W \in H) \land O (p) \in ran DIsoH (K) (W)) \to O (O (O (p))) = O (p)$
59	5 57 58	syl2an2r	$⊢ (φ \land p \in A) \to O (O (O (p))) = O (p)$
60	59	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (O (p))) = O (p)$
61	52 60	eqtrd	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) = O (p)$
62	46	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (p) \in J$
63	61 62	eqeltrd	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) \in J$
64	49 63 31	sylanbrc	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to f \in T$
65	1 2 55 9	dih1dimat	$⊢ ((K \in HL \land W \in H) \land p \in A) \to p \in ran DIsoH (K) (W)$
66	5 45 65	syl2an2r	$⊢ (φ \land p \in A) \to p \in ran DIsoH (K) (W)$
67	1 55 8	dochoc	$⊢ ((K \in HL \land W \in H) \land p \in ran DIsoH (K) (W)) \to O (O (p)) = p$
68	5 66 67	syl2an2r	$⊢ (φ \land p \in A) \to O (O (p)) = p$
69	68	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (p)) = p$
70	51 69	eqtr2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to p = O (L (f))$
71	48 64 70	reximssdv	$⊢ (φ \land p \in A) \to \exists f \in T p = O (L (f))$
72		sseq1	$⊢ p = O (L (f)) \to (p \subseteq X \leftrightarrow O (L (f)) \subseteq X)$
73		sseq1	$⊢ p = O (L (f)) \to (p \subseteq Y \leftrightarrow O (L (f)) \subseteq Y)$
74	72 73	imbi12d	$⊢ p = O (L (f)) \to ((p \subseteq X \to p \subseteq Y) \leftrightarrow (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
75	74	adantl	$⊢ (φ \land p = O (L (f))) \to ((p \subseteq X \to p \subseteq Y) \leftrightarrow (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
76	42 71 75	ralxfrd	$⊢ φ \to (\forall p \in A (p \subseteq X \to p \subseteq Y) \leftrightarrow \forall f \in T (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y))$
77	30 76	bitr2d	$⊢ φ \to (\forall f \in T (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y) \leftrightarrow X \subseteq Y)$
78	28 77	sylibd	$⊢ φ \to (\{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \to X \subseteq Y)$
79		simplr	$⊢ ((φ \land X \subseteq Y) \land f \in C) \to X \subseteq Y$
80		sstr	$⊢ (O (L (f)) \subseteq X \land X \subseteq Y) \to O (L (f)) \subseteq Y$
81	80	ancoms	$⊢ (X \subseteq Y \land O (L (f)) \subseteq X) \to O (L (f)) \subseteq Y$
82	81	a1i	$⊢ ((φ \land X \subseteq Y) \land f \in C) \to ((X \subseteq Y \land O (L (f)) \subseteq X) \to O (L (f)) \subseteq Y)$
83	79 82	mpand	$⊢ ((φ \land X \subseteq Y) \land f \in C) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)$
84	83	ss2rabdv	$⊢ (φ \land X \subseteq Y) \to \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\}$
85	84	ex	$⊢ φ \to (X \subseteq Y \to \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\})$
86	78 85	impbid	$⊢ φ \to (\{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \leftrightarrow X \subseteq Y)$
87	17 86	bitrd	$⊢ φ \to (M (X) \subseteq M (Y) \leftrightarrow X \subseteq Y)$

Metamath Proof Explorer

Theorem mapdordlem2

Proof