dihatexv

Description: There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 16-Aug-2014)

	Ref	Expression
Hypotheses	dihatexv.b	$⊢ B = {Base}_{K}$
	dihatexv.a	$⊢ A = Atoms (K)$
	dihatexv.h	$⊢ H = LHyp (K)$
	dihatexv.u	$⊢ U = DVecH (K) (W)$
	dihatexv.v	$⊢ V = {Base}_{U}$
	dihatexv.o	$⊢ \underset{˙}{0} = 0_{U}$
	dihatexv.n	$⊢ N = LSpan (U)$
	dihatexv.i	$⊢ I = DIsoH (K) (W)$
	dihatexv.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihatexv.q	$⊢ φ \to Q \in B$
Assertion	dihatexv	$⊢ φ \to (Q \in A \leftrightarrow \exists x \in (V ∖ \{\underset{˙}{0}\}) I (Q) = N (\{x\}))$

Proof

Step	Hyp	Ref	Expression
1		dihatexv.b	$⊢ B = {Base}_{K}$
2		dihatexv.a	$⊢ A = Atoms (K)$
3		dihatexv.h	$⊢ H = LHyp (K)$
4		dihatexv.u	$⊢ U = DVecH (K) (W)$
5		dihatexv.v	$⊢ V = {Base}_{U}$
6		dihatexv.o	$⊢ \underset{˙}{0} = 0_{U}$
7		dihatexv.n	$⊢ N = LSpan (U)$
8		dihatexv.i	$⊢ I = DIsoH (K) (W)$
9		dihatexv.k	$⊢ φ \to (K \in HL \land W \in H)$
10		dihatexv.q	$⊢ φ \to Q \in B$
11	9	ad2antrr	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to (K \in HL \land W \in H)$
12		simplr	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to Q \in A$
13		simpr	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to Q \leq_{K} W$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
16		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{B})$
17	1 14 2 3 15 16 4 8 7	dih1dimb2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \leq_{K} W)) \to \exists g \in LTrn (K) (W) (g \neq {I ↾}_{B} \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\}))$
18	11 12 13 17	syl12anc	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to \exists g \in LTrn (K) (W) (g \neq {I ↾}_{B} \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\}))$
19	9	ad3antrrr	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to (K \in HL \land W \in H)$
20		simpr	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to g \in LTrn (K) (W)$
21		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
22	1 3 15 21 16	tendo0cl	$⊢ (K \in HL \land W \in H) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)$
23	19 22	syl	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)$
24	3 15 21 4 5	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (g \in LTrn (K) (W) \land (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W))) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩ \in V$
25	19 20 23 24	syl12anc	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩ \in V$
26		sneq	$⊢ x = ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩ \to \{x\} = \{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\}$
27	26	fveq2d	$⊢ x = ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩ \to N (\{x\}) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\})$
28	27	rspceeqv	$⊢ (⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩ \in V \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\})) \to \exists x \in V I (Q) = N (\{x\})$
29	25 28	sylan	$⊢ ((((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\})) \to \exists x \in V I (Q) = N (\{x\})$
30	29	ex	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to (I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\}) \to \exists x \in V I (Q) = N (\{x\}))$
31	30	adantld	$⊢ (((φ \land Q \in A) \land Q \leq_{K} W) \land g \in LTrn (K) (W)) \to ((g \neq {I ↾}_{B} \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\})) \to \exists x \in V I (Q) = N (\{x\}))$
32	31	rexlimdva	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to (\exists g \in LTrn (K) (W) (g \neq {I ↾}_{B} \land I (Q) = N (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{B})⟩\})) \to \exists x \in V I (Q) = N (\{x\}))$
33	18 32	mpd	$⊢ ((φ \land Q \in A) \land Q \leq_{K} W) \to \exists x \in V I (Q) = N (\{x\})$
34	9	ad2antrr	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to (K \in HL \land W \in H)$
35		eqid	$⊢ oc (K) (W) = oc (K) (W)$
36	14 2 3 35	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W)$
37	34 36	syl	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W)$
38		simplr	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to Q \in A$
39		simpr	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to \neg Q \leq_{K} W$
40		eqid	$⊢ (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) = (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q)$
41	14 2 3 15 40	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W) \land (Q \in A \land \neg Q \leq_{K} W)) \to (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W)$
42	34 37 38 39 41	syl112anc	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W)$
43	3 15 21	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W)$
44	34 43	syl	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W)$
45	3 15 21 4 5	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land ((ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W) \land {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W))) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in V$
46	34 42 44 45	syl12anc	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in V$
47	14 2 3 35 15 8 4 7 40	dih1dimc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \leq_{K} W)) \to I (Q) = N (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})$
48	34 38 39 47	syl12anc	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to I (Q) = N (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})$
49		sneq	$⊢ x = ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \to \{x\} = \{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\}$
50	49	fveq2d	$⊢ x = ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \to N (\{x\}) = N (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})$
51	50	rspceeqv	$⊢ (⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in V \land I (Q) = N (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})) \to \exists x \in V I (Q) = N (\{x\})$
52	46 48 51	syl2anc	$⊢ ((φ \land Q \in A) \land \neg Q \leq_{K} W) \to \exists x \in V I (Q) = N (\{x\})$
53	33 52	pm2.61dan	$⊢ (φ \land Q \in A) \to \exists x \in V I (Q) = N (\{x\})$
54	9	simpld	$⊢ φ \to K \in HL$
55	54	ad3antrrr	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to K \in HL$
56		hlatl	$⊢ K \in HL \to K \in AtLat$
57	55 56	syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to K \in AtLat$
58		simpllr	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to Q \in A$
59		eqid	$⊢ 0. (K) = 0. (K)$
60	59 2	atn0	$⊢ (K \in AtLat \land Q \in A) \to Q \neq 0. (K)$
61	57 58 60	syl2anc	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to Q \neq 0. (K)$
62		sneq	$⊢ x = \underset{˙}{0} \to \{x\} = \{\underset{˙}{0}\}$
63	62	fveq2d	$⊢ x = \underset{˙}{0} \to N (\{x\}) = N (\{\underset{˙}{0}\})$
64	63	3ad2ant3	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to N (\{x\}) = N (\{\underset{˙}{0}\})$
65		simp1ll	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to φ$
66	3 4 9	dvhlmod	$⊢ φ \to U \in LMod$
67	6 7	lspsn0	$⊢ U \in LMod \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
68	65 66 67	3syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to N (\{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
69	64 68	eqtrd	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to N (\{x\}) = \{\underset{˙}{0}\}$
70		simp2	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to I (Q) = N (\{x\})$
71	59 3 8 4 6	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{\underset{˙}{0}\}$
72	65 9 71	3syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to I (0. (K)) = \{\underset{˙}{0}\}$
73	69 70 72	3eqtr4d	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to I (Q) = I (0. (K))$
74	65 9	syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to (K \in HL \land W \in H)$
75	65 10	syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to Q \in B$
76	65 54	syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to K \in HL$
77		hlop	$⊢ K \in HL \to K \in OP$
78	1 59	op0cl	$⊢ K \in OP \to 0. (K) \in B$
79	76 77 78	3syl	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to 0. (K) \in B$
80	1 3 8	dih11	$⊢ ((K \in HL \land W \in H) \land Q \in B \land 0. (K) \in B) \to (I (Q) = I (0. (K)) \leftrightarrow Q = 0. (K))$
81	74 75 79 80	syl3anc	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to (I (Q) = I (0. (K)) \leftrightarrow Q = 0. (K))$
82	73 81	mpbid	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\}) \land x = \underset{˙}{0}) \to Q = 0. (K)$
83	82	3expia	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to (x = \underset{˙}{0} \to Q = 0. (K))$
84	83	necon3d	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to (Q \neq 0. (K) \to x \neq \underset{˙}{0})$
85	61 84	mpd	$⊢ (((φ \land Q \in A) \land x \in V) \land I (Q) = N (\{x\})) \to x \neq \underset{˙}{0}$
86	85	ex	$⊢ ((φ \land Q \in A) \land x \in V) \to (I (Q) = N (\{x\}) \to x \neq \underset{˙}{0})$
87	86	ancrd	$⊢ ((φ \land Q \in A) \land x \in V) \to (I (Q) = N (\{x\}) \to (x \neq \underset{˙}{0} \land I (Q) = N (\{x\})))$
88	87	reximdva	$⊢ (φ \land Q \in A) \to (\exists x \in V I (Q) = N (\{x\}) \to \exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\})))$
89	53 88	mpd	$⊢ (φ \land Q \in A) \to \exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))$
90	89	ex	$⊢ φ \to (Q \in A \to \exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\})))$
91	9	ad2antrr	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to (K \in HL \land W \in H)$
92	10	ad2antrr	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to Q \in B$
93	1 3 8	dihcnvid1	$⊢ ((K \in HL \land W \in H) \land Q \in B) \to I^{-1} (I (Q)) = Q$
94	91 92 93	syl2anc	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to I^{-1} (I (Q)) = Q$
95		fveq2	$⊢ I (Q) = N (\{x\}) \to I^{-1} (I (Q)) = I^{-1} (N (\{x\}))$
96	95	ad2antll	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to I^{-1} (I (Q)) = I^{-1} (N (\{x\}))$
97	94 96	eqtr3d	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to Q = I^{-1} (N (\{x\}))$
98	66	ad2antrr	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to U \in LMod$
99		simplr	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to x \in V$
100		simprl	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to x \neq \underset{˙}{0}$
101		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
102	5 7 6 101	lsatlspsn2	$⊢ (U \in LMod \land x \in V \land x \neq \underset{˙}{0}) \to N (\{x\}) \in LSAtoms (U)$
103	98 99 100 102	syl3anc	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to N (\{x\}) \in LSAtoms (U)$
104	2 3 4 8 101	dihlatat	$⊢ ((K \in HL \land W \in H) \land N (\{x\}) \in LSAtoms (U)) \to I^{-1} (N (\{x\})) \in A$
105	91 103 104	syl2anc	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to I^{-1} (N (\{x\})) \in A$
106	97 105	eqeltrd	$⊢ ((φ \land x \in V) \land (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))) \to Q \in A$
107	106	ex	$⊢ (φ \land x \in V) \to ((x \neq \underset{˙}{0} \land I (Q) = N (\{x\})) \to Q \in A)$
108	107	rexlimdva	$⊢ φ \to (\exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\})) \to Q \in A)$
109	90 108	impbid	$⊢ φ \to (Q \in A \leftrightarrow \exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\})))$
110		rexdifsn	$⊢ \exists x \in (V ∖ \{\underset{˙}{0}\}) I (Q) = N (\{x\}) \leftrightarrow \exists x \in V (x \neq \underset{˙}{0} \land I (Q) = N (\{x\}))$
111	109 110	bitr4di	$⊢ φ \to (Q \in A \leftrightarrow \exists x \in (V ∖ \{\underset{˙}{0}\}) I (Q) = N (\{x\}))$

Metamath Proof Explorer

Theorem dihatexv

Proof