dihlspsnat

Description: The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dihlspsnat.a	$⊢ A = Atoms (K)$
	dihlspsnat.h	$⊢ H = LHyp (K)$
	dihlspsnat.u	$⊢ U = DVecH (K) (W)$
	dihlspsnat.v	$⊢ V = {Base}_{U}$
	dihlspsnat.o	$⊢ \underset{˙}{0} = 0_{U}$
	dihlspsnat.n	$⊢ N = LSpan (U)$
	dihlspsnat.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihlspsnat	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I^{-1} (N (\{X\})) \in A$

Proof

Step	Hyp	Ref	Expression
1		dihlspsnat.a	$⊢ A = Atoms (K)$
2		dihlspsnat.h	$⊢ H = LHyp (K)$
3		dihlspsnat.u	$⊢ U = DVecH (K) (W)$
4		dihlspsnat.v	$⊢ V = {Base}_{U}$
5		dihlspsnat.o	$⊢ \underset{˙}{0} = 0_{U}$
6		dihlspsnat.n	$⊢ N = LSpan (U)$
7		dihlspsnat.i	$⊢ I = DIsoH (K) (W)$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ LSubSp (U) = LSubSp (U)$
10	8 2 7 3 9	dihf11	$⊢ (K \in HL \land W \in H) \to I : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
11	10	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
12		f1f1orn	$⊢ I : {Base}_{K} \underset{1-1}{⟶} LSubSp (U) \to I : {Base}_{K} \underset{1-1 onto}{⟶} ran I$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I : {Base}_{K} \underset{1-1 onto}{⟶} ran I$
14	2 3 4 6 7	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$
15	14	3adant3	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) \in ran I$
16		f1ocnvdm	$⊢ (I : {Base}_{K} \underset{1-1 onto}{⟶} ran I \land N (\{X\}) \in ran I) \to I^{-1} (N (\{X\})) \in {Base}_{K}$
17	13 15 16	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I^{-1} (N (\{X\})) \in {Base}_{K}$
18		fveq2	$⊢ I^{-1} (N (\{X\})) = 0. (K) \to I (I^{-1} (N (\{X\}))) = I (0. (K))$
19	2 7	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land N (\{X\}) \in ran I) \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
20	14 19	syldan	$⊢ ((K \in HL \land W \in H) \land X \in V) \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
21		eqid	$⊢ 0. (K) = 0. (K)$
22	21 2 7 3 5	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{\underset{˙}{0}\}$
23	22	adantr	$⊢ ((K \in HL \land W \in H) \land X \in V) \to I (0. (K)) = \{\underset{˙}{0}\}$
24	20 23	eqeq12d	$⊢ ((K \in HL \land W \in H) \land X \in V) \to (I (I^{-1} (N (\{X\}))) = I (0. (K)) \leftrightarrow N (\{X\}) = \{\underset{˙}{0}\})$
25		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
26	2 3 25	dvhlmod	$⊢ (K \in HL \land W \in H) \to U \in LMod$
27	4 5 6	lspsneq0	$⊢ (U \in LMod \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
28	26 27	sylan	$⊢ ((K \in HL \land W \in H) \land X \in V) \to (N (\{X\}) = \{\underset{˙}{0}\} \leftrightarrow X = \underset{˙}{0})$
29	24 28	bitrd	$⊢ ((K \in HL \land W \in H) \land X \in V) \to (I (I^{-1} (N (\{X\}))) = I (0. (K)) \leftrightarrow X = \underset{˙}{0})$
30	18 29	syl5ib	$⊢ ((K \in HL \land W \in H) \land X \in V) \to (I^{-1} (N (\{X\})) = 0. (K) \to X = \underset{˙}{0})$
31	30	necon3d	$⊢ ((K \in HL \land W \in H) \land X \in V) \to (X \neq \underset{˙}{0} \to I^{-1} (N (\{X\})) \neq 0. (K))$
32	31	3impia	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I^{-1} (N (\{X\})) \neq 0. (K)$
33		simpll1	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to (K \in HL \land W \in H)$
34	2 3 33	dvhlvec	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to U \in LVec$
35		simplr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to x \in {Base}_{K}$
36	8 2 7 3 9	dihlss	$⊢ ((K \in HL \land W \in H) \land x \in {Base}_{K}) \to I (x) \in LSubSp (U)$
37	33 35 36	syl2anc	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to I (x) \in LSubSp (U)$
38		simpll2	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to X \in V$
39		simpr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to I (x) \subseteq N (\{X\})$
40	4 5 9 6	lspsnat	$⊢ ((U \in LVec \land I (x) \in LSubSp (U) \land X \in V) \land I (x) \subseteq N (\{X\})) \to (I (x) = N (\{X\}) \lor I (x) = \{\underset{˙}{0}\})$
41	34 37 38 39 40	syl31anc	$⊢ ((((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \land I (x) \subseteq N (\{X\})) \to (I (x) = N (\{X\}) \lor I (x) = \{\underset{˙}{0}\})$
42	41	ex	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) \subseteq N (\{X\}) \to (I (x) = N (\{X\}) \lor I (x) = \{\underset{˙}{0}\}))$
43		simp1	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to (K \in HL \land W \in H)$
44	43 15 19	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
45	44	adantr	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
46	45	sseq2d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) \subseteq I (I^{-1} (N (\{X\}))) \leftrightarrow I (x) \subseteq N (\{X\}))$
47		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (K \in HL \land W \in H)$
48		simpr	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to x \in {Base}_{K}$
49	17	adantr	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to I^{-1} (N (\{X\})) \in {Base}_{K}$
50		eqid	$⊢ \leq_{K} = \leq_{K}$
51	8 50 2 7	dihord	$⊢ ((K \in HL \land W \in H) \land x \in {Base}_{K} \land I^{-1} (N (\{X\})) \in {Base}_{K}) \to (I (x) \subseteq I (I^{-1} (N (\{X\}))) \leftrightarrow x \leq_{K} I^{-1} (N (\{X\})))$
52	47 48 49 51	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) \subseteq I (I^{-1} (N (\{X\}))) \leftrightarrow x \leq_{K} I^{-1} (N (\{X\})))$
53	46 52	bitr3d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) \subseteq N (\{X\}) \leftrightarrow x \leq_{K} I^{-1} (N (\{X\})))$
54	45	eqeq2d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = I (I^{-1} (N (\{X\}))) \leftrightarrow I (x) = N (\{X\}))$
55	8 2 7	dih11	$⊢ ((K \in HL \land W \in H) \land x \in {Base}_{K} \land I^{-1} (N (\{X\})) \in {Base}_{K}) \to (I (x) = I (I^{-1} (N (\{X\}))) \leftrightarrow x = I^{-1} (N (\{X\})))$
56	47 48 49 55	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = I (I^{-1} (N (\{X\}))) \leftrightarrow x = I^{-1} (N (\{X\})))$
57	54 56	bitr3d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = N (\{X\}) \leftrightarrow x = I^{-1} (N (\{X\})))$
58	47 22	syl	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to I (0. (K)) = \{\underset{˙}{0}\}$
59	58	eqeq2d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = I (0. (K)) \leftrightarrow I (x) = \{\underset{˙}{0}\})$
60		simpl1l	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to K \in HL$
61		hlop	$⊢ K \in HL \to K \in OP$
62	8 21	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
63	60 61 62	3syl	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to 0. (K) \in {Base}_{K}$
64	8 2 7	dih11	$⊢ ((K \in HL \land W \in H) \land x \in {Base}_{K} \land 0. (K) \in {Base}_{K}) \to (I (x) = I (0. (K)) \leftrightarrow x = 0. (K))$
65	47 48 63 64	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = I (0. (K)) \leftrightarrow x = 0. (K))$
66	59 65	bitr3d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (I (x) = \{\underset{˙}{0}\} \leftrightarrow x = 0. (K))$
67	57 66	orbi12d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to ((I (x) = N (\{X\}) \lor I (x) = \{\underset{˙}{0}\}) \leftrightarrow (x = I^{-1} (N (\{X\})) \lor x = 0. (K)))$
68	42 53 67	3imtr3d	$⊢ (((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \land x \in {Base}_{K}) \to (x \leq_{K} I^{-1} (N (\{X\})) \to (x = I^{-1} (N (\{X\})) \lor x = 0. (K)))$
69	68	ralrimiva	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to \forall x \in {Base}_{K} (x \leq_{K} I^{-1} (N (\{X\})) \to (x = I^{-1} (N (\{X\})) \lor x = 0. (K)))$
70		simp1l	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to K \in HL$
71		hlatl	$⊢ K \in HL \to K \in AtLat$
72	8 50 21 1	isat3	$⊢ K \in AtLat \to (I^{-1} (N (\{X\})) \in A \leftrightarrow (I^{-1} (N (\{X\})) \in {Base}_{K} \land I^{-1} (N (\{X\})) \neq 0. (K) \land \forall x \in {Base}_{K} (x \leq_{K} I^{-1} (N (\{X\})) \to (x = I^{-1} (N (\{X\})) \lor x = 0. (K)))))$
73	70 71 72	3syl	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to (I^{-1} (N (\{X\})) \in A \leftrightarrow (I^{-1} (N (\{X\})) \in {Base}_{K} \land I^{-1} (N (\{X\})) \neq 0. (K) \land \forall x \in {Base}_{K} (x \leq_{K} I^{-1} (N (\{X\})) \to (x = I^{-1} (N (\{X\})) \lor x = 0. (K)))))$
74	17 32 69 73	mpbir3and	$⊢ ((K \in HL \land W \in H) \land X \in V \land X \neq \underset{˙}{0}) \to I^{-1} (N (\{X\})) \in A$

Metamath Proof Explorer

Theorem dihlspsnat

Proof