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	43	adantr	$⊢ (φ \land p \in A) \to U \in LVec$
45	5	adantr	$⊢ (φ \land p \in A) \to (K \in HL \land W \in H)$
46		simpr	$⊢ (φ \land p \in A) \to p \in A$
47	1 2 8 9 11 45 46	dochsatshp	$⊢ (φ \land p \in A) \to O (p) \in J$
48	11 10 12	lshpkrex	$⊢ (U \in LVec \land O (p) \in J) \to \exists f \in F L (f) = O (p)$
49	44 47 48	syl2anc	$⊢ (φ \land p \in A) \to \exists f \in F L (f) = O (p)$
50		df-rex	$⊢ \exists f \in F L (f) = O (p) \leftrightarrow \exists f (f \in F \land L (f) = O (p))$
51	49 50	sylib	$⊢ (φ \land p \in A) \to \exists f (f \in F \land L (f) = O (p))$
52		simprl	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to f \in F$
53		simprr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to L (f) = O (p)$
54	53	fveq2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (L (f)) = O (O (p))$
55	54	fveq2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) = O (O (O (p)))$
56	29	adantr	$⊢ (φ \land p \in A) \to U \in LMod$
57	19 9 56 46	lsatssv	$⊢ (φ \land p \in A) \to p \subseteq {Base}_{U}$
58		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
59	1 58 2 19 8	dochcl	$⊢ ((K \in HL \land W \in H) \land p \subseteq {Base}_{U}) \to O (p) \in ran DIsoH (K) (W)$
60	45 57 59	syl2anc	$⊢ (φ \land p \in A) \to O (p) \in ran DIsoH (K) (W)$
61	1 58 8	dochoc	$⊢ ((K \in HL \land W \in H) \land O (p) \in ran DIsoH (K) (W)) \to O (O (O (p))) = O (p)$
62	45 60 61	syl2anc	$⊢ (φ \land p \in A) \to O (O (O (p))) = O (p)$
63	62	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (O (p))) = O (p)$
64	55 63	eqtrd	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) = O (p)$
65	47	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (p) \in J$
66	64 65	eqeltrd	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (L (f))) \in J$
67	52 66 31	sylanbrc	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to f \in T$
68	1 2 58 9	dih1dimat	$⊢ ((K \in HL \land W \in H) \land p \in A) \to p \in ran DIsoH (K) (W)$
69	45 46 68	syl2anc	$⊢ (φ \land p \in A) \to p \in ran DIsoH (K) (W)$
70	1 58 8	dochoc	$⊢ ((K \in HL \land W \in H) \land p \in ran DIsoH (K) (W)) \to O (O (p)) = p$
71	45 69 70	syl2anc	$⊢ (φ \land p \in A) \to O (O (p)) = p$
72	71	adantr	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to O (O (p)) = p$
73	54 72	eqtr2d	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to p = O (L (f))$
74	67 73	jca	$⊢ ((φ \land p \in A) \land (f \in F \land L (f) = O (p))) \to (f \in T \land p = O (L (f)))$
75	74	ex	$⊢ (φ \land p \in A) \to ((f \in F \land L (f) = O (p)) \to (f \in T \land p = O (L (f))))$
76	75	eximdv	$⊢ (φ \land p \in A) \to (\exists f (f \in F \land L (f) = O (p)) \to \exists f (f \in T \land p = O (L (f))))$
77	51 76	mpd	$⊢ (φ \land p \in A) \to \exists f (f \in T \land p = O (L (f)))$
78		df-rex	$⊢ \exists f \in T p = O (L (f)) \leftrightarrow \exists f (f \in T \land p = O (L (f)))$
79	77 78	sylibr	$⊢ (φ \land p \in A) \to \exists f \in T p = O (L (f))$
80		sseq1	$⊢ p = O (L (f)) \to (p \subseteq X \leftrightarrow O (L (f)) \subseteq X)$
81		sseq1	$⊢ p = O (L (f)) \to (p \subseteq Y \leftrightarrow O (L (f)) \subseteq Y)$
82	80 81	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))$
83	82	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))$
84	42 79 83	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))$
85	30 84	bitr2d	$⊢ φ \to (\forall f \in T (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y) \leftrightarrow X \subseteq Y)$
86	28 85	sylibd	$⊢ φ \to (\{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \to X \subseteq Y)$
87		simplr	$⊢ ((φ \land X \subseteq Y) \land f \in C) \to X \subseteq Y$
88		sstr	$⊢ (O (L (f)) \subseteq X \land X \subseteq Y) \to O (L (f)) \subseteq Y$
89	88	ancoms	$⊢ (X \subseteq Y \land O (L (f)) \subseteq X) \to O (L (f)) \subseteq Y$
90	89	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)$
91	87 90	mpand	$⊢ ((φ \land X \subseteq Y) \land f \in C) \to (O (L (f)) \subseteq X \to O (L (f)) \subseteq Y)$
92	91	ss2rabdv	$⊢ (φ \land X \subseteq Y) \to \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\}$
93	92	ex	$⊢ φ \to (X \subseteq Y \to \{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\})$
94	86 93	impbid	$⊢ φ \to (\{f \in C \| O (L (f)) \subseteq X\} \subseteq \{f \in C \| O (L (f)) \subseteq Y\} \leftrightarrow X \subseteq Y)$
95	17 94	bitrd	$⊢ φ \to (M (X) \subseteq M (Y) \leftrightarrow X \subseteq Y)$

Metamath Proof Explorer

Theorem mapdordlem2

Proof