dih1

Description: The value of isomorphism H at the lattice unity is the set of all vectors. (Contributed by NM, 13-Mar-2014)

	Ref	Expression
Hypotheses	dih1.m	$⊢ \underset{˙}{1} = 1. (K)$
	dih1.h	$⊢ H = LHyp (K)$
	dih1.i	$⊢ I = DIsoH (K) (W)$
	dih1.u	$⊢ U = DVecH (K) (W)$
	dih1.v	$⊢ V = {Base}_{U}$
Assertion	dih1	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{1}) = V$

Proof

Step	Hyp	Ref	Expression
1		dih1.m	$⊢ \underset{˙}{1} = 1. (K)$
2		dih1.h	$⊢ H = LHyp (K)$
3		dih1.i	$⊢ I = DIsoH (K) (W)$
4		dih1.u	$⊢ U = DVecH (K) (W)$
5		dih1.v	$⊢ V = {Base}_{U}$
6	2 3	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (\underset{˙}{1})$
7		relxp	$⊢ Rel (LTrn (K) (W) \times TEndo (K) (W))$
8		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
9		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
10	2 8 9 4 5	dvhvbase	$⊢ (K \in HL \land W \in H) \to V = LTrn (K) (W) \times TEndo (K) (W)$
11	10	releqd	$⊢ (K \in HL \land W \in H) \to (Rel V \leftrightarrow Rel (LTrn (K) (W) \times TEndo (K) (W)))$
12	7 11	mpbiri	$⊢ (K \in HL \land W \in H) \to Rel V$
13		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
14		hlop	$⊢ K \in HL \to K \in OP$
15	14	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to K \in OP$
16		simpl	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to (K \in HL \land W \in H)$
17		simprl	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to f \in LTrn (K) (W)$
18		simprr	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to s \in TEndo (K) (W)$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20		eqid	$⊢ oc (K) = oc (K)$
21		eqid	$⊢ Atoms (K) = Atoms (K)$
22	19 20 21 2	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in Atoms (K) \land \neg oc (K) (W) \leq_{K} W)$
23	22	adantr	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to (oc (K) (W) \in Atoms (K) \land \neg oc (K) (W) \leq_{K} W)$
24		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W))$
25	19 21 2 8 24	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in Atoms (K) \land \neg oc (K) (W) \leq_{K} W) \land (oc (K) (W) \in Atoms (K) \land \neg oc (K) (W) \leq_{K} W)) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)) \in LTrn (K) (W)$
26	16 23 23 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)) \in LTrn (K) (W)$
27	2 8 9	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in TEndo (K) (W) \land (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)) \in LTrn (K) (W)) \to s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W))) \in LTrn (K) (W)$
28	16 18 26 27	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W))) \in LTrn (K) (W)$
29	2 8	ltrncnv	$⊢ ((K \in HL \land W \in H) \land s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W))) \in LTrn (K) (W)) \to {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)$
30	28 29	syldan	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)$
31	2 8	ltrnco	$⊢ ((K \in HL \land W \in H) \land f \in LTrn (K) (W) \land {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)) \to f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)$
32	16 17 30 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)$
33		eqid	$⊢ {Base}_{K} = {Base}_{K}$
34		eqid	$⊢ trL (K) (W) = trL (K) (W)$
35	33 2 8 34	trlcl	$⊢ ((K \in HL \land W \in H) \land f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1} \in LTrn (K) (W)) \to trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \in {Base}_{K}$
36	32 35	syldan	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \in {Base}_{K}$
37	33 19 1	ople1	$⊢ (K \in OP \land trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \in {Base}_{K}) \to trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1}$
38	15 36 37	syl2anc	$⊢ ((K \in HL \land W \in H) \land (f \in LTrn (K) (W) \land s \in TEndo (K) (W))) \to trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1}$
39	38	ex	$⊢ (K \in HL \land W \in H) \to ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \to trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1})$
40	39	pm4.71d	$⊢ (K \in HL \land W \in H) \to ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \leftrightarrow ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1}))$
41	10	eleq2d	$⊢ (K \in HL \land W \in H) \to (⟨f, s⟩ \in V \leftrightarrow ⟨f, s⟩ \in (LTrn (K) (W) \times TEndo (K) (W)))$
42		opelxp	$⊢ ⟨f, s⟩ \in (LTrn (K) (W) \times TEndo (K) (W)) \leftrightarrow (f \in LTrn (K) (W) \land s \in TEndo (K) (W))$
43	41 42	bitrdi	$⊢ (K \in HL \land W \in H) \to (⟨f, s⟩ \in V \leftrightarrow (f \in LTrn (K) (W) \land s \in TEndo (K) (W)))$
44	14	adantr	$⊢ (K \in HL \land W \in H) \to K \in OP$
45	33 1	op1cl	$⊢ K \in OP \to \underset{˙}{1} \in {Base}_{K}$
46	44 45	syl	$⊢ (K \in HL \land W \in H) \to \underset{˙}{1} \in {Base}_{K}$
47		hlpos	$⊢ K \in HL \to K \in Poset$
48	47	adantr	$⊢ (K \in HL \land W \in H) \to K \in Poset$
49	33 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
50	49	adantl	$⊢ (K \in HL \land W \in H) \to W \in {Base}_{K}$
51		eqid	$⊢ ⋖_{K} = ⋖_{K}$
52	1 51 2	lhp1cvr	$⊢ (K \in HL \land W \in H) \to W ⋖_{K} \underset{˙}{1}$
53	33 19 51	cvrnle	$⊢ ((K \in Poset \land W \in {Base}_{K} \land \underset{˙}{1} \in {Base}_{K}) \land W ⋖_{K} \underset{˙}{1}) \to \neg \underset{˙}{1} \leq_{K} W$
54	48 50 46 52 53	syl31anc	$⊢ (K \in HL \land W \in H) \to \neg \underset{˙}{1} \leq_{K} W$
55		hlol	$⊢ K \in HL \to K \in OL$
56		eqid	$⊢ meet (K) = meet (K)$
57	33 56 1	olm12	$⊢ (K \in OL \land W \in {Base}_{K}) \to \underset{˙}{1} meet (K) W = W$
58	55 49 57	syl2an	$⊢ (K \in HL \land W \in H) \to \underset{˙}{1} meet (K) W = W$
59	58	oveq2d	$⊢ (K \in HL \land W \in H) \to oc (K) (W) join (K) (\underset{˙}{1} meet (K) W) = oc (K) (W) join (K) W$
60		hllat	$⊢ K \in HL \to K \in Lat$
61	60	adantr	$⊢ (K \in HL \land W \in H) \to K \in Lat$
62	33 20	opoccl	$⊢ (K \in OP \land W \in {Base}_{K}) \to oc (K) (W) \in {Base}_{K}$
63	14 49 62	syl2an	$⊢ (K \in HL \land W \in H) \to oc (K) (W) \in {Base}_{K}$
64		eqid	$⊢ join (K) = join (K)$
65	33 64	latjcom	$⊢ (K \in Lat \land oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K}) \to oc (K) (W) join (K) W = W join (K) oc (K) (W)$
66	61 63 50 65	syl3anc	$⊢ (K \in HL \land W \in H) \to oc (K) (W) join (K) W = W join (K) oc (K) (W)$
67	33 20 64 1	opexmid	$⊢ (K \in OP \land W \in {Base}_{K}) \to W join (K) oc (K) (W) = \underset{˙}{1}$
68	14 49 67	syl2an	$⊢ (K \in HL \land W \in H) \to W join (K) oc (K) (W) = \underset{˙}{1}$
69	59 66 68	3eqtrd	$⊢ (K \in HL \land W \in H) \to oc (K) (W) join (K) (\underset{˙}{1} meet (K) W) = \underset{˙}{1}$
70		eqid	$⊢ oc (K) (W) = oc (K) (W)$
71		vex	$⊢ f \in V$
72		vex	$⊢ s \in V$
73	33 19 64 56 21 2 70 8 34 9 3 24 71 72	dihopelvalc	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{1} \in {Base}_{K} \land \neg \underset{˙}{1} \leq_{K} W) \land ((oc (K) (W) \in Atoms (K) \land \neg oc (K) (W) \leq_{K} W) \land oc (K) (W) join (K) (\underset{˙}{1} meet (K) W) = \underset{˙}{1})) \to (⟨f, s⟩ \in I (\underset{˙}{1}) \leftrightarrow ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1}))$
74	13 46 54 22 69 73	syl122anc	$⊢ (K \in HL \land W \in H) \to (⟨f, s⟩ \in I (\underset{˙}{1}) \leftrightarrow ((f \in LTrn (K) (W) \land s \in TEndo (K) (W)) \land trL (K) (W) (f \circ {s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = oc (K) (W)))}^{-1}) \leq_{K} \underset{˙}{1}))$
75	40 43 74	3bitr4rd	$⊢ (K \in HL \land W \in H) \to (⟨f, s⟩ \in I (\underset{˙}{1}) \leftrightarrow ⟨f, s⟩ \in V)$
76	75	eqrelrdv2	$⊢ ((Rel I (\underset{˙}{1}) \land Rel V) \land (K \in HL \land W \in H)) \to I (\underset{˙}{1}) = V$
77	6 12 13 76	syl21anc	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{1}) = V$

Metamath Proof Explorer

Theorem dih1

Proof