Theorem dia2dimlem3

Description: Lemma for dia2dim . Define a translation D whose trace is atom V . Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem3.l	|- .<_ = ( le ` K )
	dia2dimlem3.j	|- .\/ = ( join ` K )
	dia2dimlem3.m	|- ./\ = ( meet ` K )
	dia2dimlem3.a	|- A = ( Atoms ` K )
	dia2dimlem3.h	|- H = ( LHyp ` K )
	dia2dimlem3.t	|- T = ( ( LTrn ` K ) ` W )
	dia2dimlem3.r	|- R = ( ( trL ` K ) ` W )
	dia2dimlem3.q	|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
	dia2dimlem3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dia2dimlem3.u	|- ( ph -> ( U e. A /\ U .<_ W ) )
	dia2dimlem3.v	|- ( ph -> ( V e. A /\ V .<_ W ) )
	dia2dimlem3.p	|- ( ph -> ( P e. A /\ -. P .<_ W ) )
	dia2dimlem3.f	|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
	dia2dimlem3.rf	|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
	dia2dimlem3.uv	|- ( ph -> U =/= V )
	dia2dimlem3.ru	|- ( ph -> ( R ` F ) =/= U )
	dia2dimlem3.rv	|- ( ph -> ( R ` F ) =/= V )
	dia2dimlem3.d	|- ( ph -> D e. T )
	dia2dimlem3.dv	|- ( ph -> ( D ` Q ) = ( F ` P ) )
Assertion	dia2dimlem3	|- ( ph -> ( R ` D ) = V )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem3.l	|- .<_ = ( le ` K )
2		dia2dimlem3.j	|- .\/ = ( join ` K )
3		dia2dimlem3.m	|- ./\ = ( meet ` K )
4		dia2dimlem3.a	|- A = ( Atoms ` K )
5		dia2dimlem3.h	|- H = ( LHyp ` K )
6		dia2dimlem3.t	|- T = ( ( LTrn ` K ) ` W )
7		dia2dimlem3.r	|- R = ( ( trL ` K ) ` W )
8		dia2dimlem3.q	|- Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) )
9		dia2dimlem3.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		dia2dimlem3.u	|- ( ph -> ( U e. A /\ U .<_ W ) )
11		dia2dimlem3.v	|- ( ph -> ( V e. A /\ V .<_ W ) )
12		dia2dimlem3.p	|- ( ph -> ( P e. A /\ -. P .<_ W ) )
13		dia2dimlem3.f	|- ( ph -> ( F e. T /\ ( F ` P ) =/= P ) )
14		dia2dimlem3.rf	|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
15		dia2dimlem3.uv	|- ( ph -> U =/= V )
16		dia2dimlem3.ru	|- ( ph -> ( R ` F ) =/= U )
17		dia2dimlem3.rv	|- ( ph -> ( R ` F ) =/= V )
18		dia2dimlem3.d	|- ( ph -> D e. T )
19		dia2dimlem3.dv	|- ( ph -> ( D ` Q ) = ( F ` P ) )
20	9	simpld	|- ( ph -> K e. HL )
21	13	simpld	|- ( ph -> F e. T )
22	1 4 5 6	ltrnel	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
23	9 21 12 22	syl3anc	|- ( ph -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
24	23	simpld	|- ( ph -> ( F ` P ) e. A )
25	11	simpld	|- ( ph -> V e. A )
26	1 2 4	hlatlej2	|- ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> V .<_ ( ( F ` P ) .\/ V ) )
27	20 24 25 26	syl3anc	|- ( ph -> V .<_ ( ( F ` P ) .\/ V ) )
28	20	hllatd	|- ( ph -> K e. Lat )
29		eqid	|- ( Base ` K ) = ( Base ` K )
30	29 4	atbase	|- ( V e. A -> V e. ( Base ` K ) )
31	25 30	syl	|- ( ph -> V e. ( Base ` K ) )
32	29 2 4	hlatjcl	|- ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
33	20 24 25 32	syl3anc	|- ( ph -> ( ( F ` P ) .\/ V ) e. ( Base ` K ) )
34	1 4 5 6 7	trlat	|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F e. T /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
35	9 12 13 34	syl3anc	|- ( ph -> ( R ` F ) e. A )
36	10	simpld	|- ( ph -> U e. A )
37	29 2 4	hlatjcl	|- ( ( K e. HL /\ ( R ` F ) e. A /\ U e. A ) -> ( ( R ` F ) .\/ U ) e. ( Base ` K ) )
38	20 35 36 37	syl3anc	|- ( ph -> ( ( R ` F ) .\/ U ) e. ( Base ` K ) )
39	29 1 3	latmlem2	|- ( ( K e. Lat /\ ( V e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) /\ ( ( R ` F ) .\/ U ) e. ( Base ` K ) ) ) -> ( V .<_ ( ( F ` P ) .\/ V ) -> ( ( ( R ` F ) .\/ U ) ./\ V ) .<_ ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) )
40	28 31 33 38 39	syl13anc	|- ( ph -> ( V .<_ ( ( F ` P ) .\/ V ) -> ( ( ( R ` F ) .\/ U ) ./\ V ) .<_ ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ) )
41	27 40	mpd	|- ( ph -> ( ( ( R ` F ) .\/ U ) ./\ V ) .<_ ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
42	2 4	hlatjcom	|- ( ( K e. HL /\ U e. A /\ V e. A ) -> ( U .\/ V ) = ( V .\/ U ) )
43	20 36 25 42	syl3anc	|- ( ph -> ( U .\/ V ) = ( V .\/ U ) )
44	14 43	breqtrd	|- ( ph -> ( R ` F ) .<_ ( V .\/ U ) )
45	1 2 4	hlatexch2	|- ( ( K e. HL /\ ( ( R ` F ) e. A /\ V e. A /\ U e. A ) /\ ( R ` F ) =/= U ) -> ( ( R ` F ) .<_ ( V .\/ U ) -> V .<_ ( ( R ` F ) .\/ U ) ) )
46	20 35 25 36 16 45	syl131anc	|- ( ph -> ( ( R ` F ) .<_ ( V .\/ U ) -> V .<_ ( ( R ` F ) .\/ U ) ) )
47	44 46	mpd	|- ( ph -> V .<_ ( ( R ` F ) .\/ U ) )
48	29 1 3	latleeqm2	|- ( ( K e. Lat /\ V e. ( Base ` K ) /\ ( ( R ` F ) .\/ U ) e. ( Base ` K ) ) -> ( V .<_ ( ( R ` F ) .\/ U ) <-> ( ( ( R ` F ) .\/ U ) ./\ V ) = V ) )
49	28 31 38 48	syl3anc	|- ( ph -> ( V .<_ ( ( R ` F ) .\/ U ) <-> ( ( ( R ` F ) .\/ U ) ./\ V ) = V ) )
50	47 49	mpbid	|- ( ph -> ( ( ( R ` F ) .\/ U ) ./\ V ) = V )
51	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dia2dimlem1	|- ( ph -> ( Q e. A /\ -. Q .<_ W ) )
52	1 2 3 4 5 6 7	trlval2	|- ( ( ( K e. HL /\ W e. H ) /\ D e. T /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( R ` D ) = ( ( Q .\/ ( D ` Q ) ) ./\ W ) )
53	9 18 51 52	syl3anc	|- ( ph -> ( R ` D ) = ( ( Q .\/ ( D ` Q ) ) ./\ W ) )
54	8	a1i	|- ( ph -> Q = ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
55	54 19	oveq12d	|- ( ph -> ( Q .\/ ( D ` Q ) ) = ( ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .\/ ( F ` P ) ) )
56	12	simpld	|- ( ph -> P e. A )
57	29 2 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ U e. A ) -> ( P .\/ U ) e. ( Base ` K ) )
58	20 56 36 57	syl3anc	|- ( ph -> ( P .\/ U ) e. ( Base ` K ) )
59	1 2 4	hlatlej1	|- ( ( K e. HL /\ ( F ` P ) e. A /\ V e. A ) -> ( F ` P ) .<_ ( ( F ` P ) .\/ V ) )
60	20 24 25 59	syl3anc	|- ( ph -> ( F ` P ) .<_ ( ( F ` P ) .\/ V ) )
61	29 1 2 3 4	atmod4i1	|- ( ( K e. HL /\ ( ( F ` P ) e. A /\ ( P .\/ U ) e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) ) /\ ( F ` P ) .<_ ( ( F ` P ) .\/ V ) ) -> ( ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .\/ ( F ` P ) ) = ( ( ( P .\/ U ) .\/ ( F ` P ) ) ./\ ( ( F ` P ) .\/ V ) ) )
62	20 24 58 33 60 61	syl131anc	|- ( ph -> ( ( ( P .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) .\/ ( F ` P ) ) = ( ( ( P .\/ U ) .\/ ( F ` P ) ) ./\ ( ( F ` P ) .\/ V ) ) )
63	2 4	hlatj32	|- ( ( K e. HL /\ ( P e. A /\ U e. A /\ ( F ` P ) e. A ) ) -> ( ( P .\/ U ) .\/ ( F ` P ) ) = ( ( P .\/ ( F ` P ) ) .\/ U ) )
64	20 56 36 24 63	syl13anc	|- ( ph -> ( ( P .\/ U ) .\/ ( F ` P ) ) = ( ( P .\/ ( F ` P ) ) .\/ U ) )
65	64	oveq1d	|- ( ph -> ( ( ( P .\/ U ) .\/ ( F ` P ) ) ./\ ( ( F ` P ) .\/ V ) ) = ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
66	55 62 65	3eqtrd	|- ( ph -> ( Q .\/ ( D ` Q ) ) = ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
67	66	oveq1d	|- ( ph -> ( ( Q .\/ ( D ` Q ) ) ./\ W ) = ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ./\ W ) )
68		hlol	|- ( K e. HL -> K e. OL )
69	20 68	syl	|- ( ph -> K e. OL )
70	29 2 4	hlatjcl	|- ( ( K e. HL /\ P e. A /\ ( F ` P ) e. A ) -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
71	20 56 24 70	syl3anc	|- ( ph -> ( P .\/ ( F ` P ) ) e. ( Base ` K ) )
72	29 4	atbase	|- ( U e. A -> U e. ( Base ` K ) )
73	36 72	syl	|- ( ph -> U e. ( Base ` K ) )
74	29 2	latjcl	|- ( ( K e. Lat /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( P .\/ ( F ` P ) ) .\/ U ) e. ( Base ` K ) )
75	28 71 73 74	syl3anc	|- ( ph -> ( ( P .\/ ( F ` P ) ) .\/ U ) e. ( Base ` K ) )
76	9	simprd	|- ( ph -> W e. H )
77	29 5	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
78	76 77	syl	|- ( ph -> W e. ( Base ` K ) )
79	29 3	latm32	|- ( ( K e. OL /\ ( ( ( P .\/ ( F ` P ) ) .\/ U ) e. ( Base ` K ) /\ ( ( F ` P ) .\/ V ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ./\ W ) = ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) ./\ ( ( F ` P ) .\/ V ) ) )
80	69 75 33 78 79	syl13anc	|- ( ph -> ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) ./\ W ) = ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) ./\ ( ( F ` P ) .\/ V ) ) )
81	1 2 3 4 5 6 7	trlval2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
82	9 21 12 81	syl3anc	|- ( ph -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
83	82	oveq1d	|- ( ph -> ( ( R ` F ) .\/ U ) = ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ U ) )
84	10	simprd	|- ( ph -> U .<_ W )
85	29 1 2 3 4	atmod4i1	|- ( ( K e. HL /\ ( U e. A /\ ( P .\/ ( F ` P ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ U .<_ W ) -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ U ) = ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) )
86	20 36 71 78 84 85	syl131anc	|- ( ph -> ( ( ( P .\/ ( F ` P ) ) ./\ W ) .\/ U ) = ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) )
87	83 86	eqtr2d	|- ( ph -> ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) = ( ( R ` F ) .\/ U ) )
88	87	oveq1d	|- ( ph -> ( ( ( ( P .\/ ( F ` P ) ) .\/ U ) ./\ W ) ./\ ( ( F ` P ) .\/ V ) ) = ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
89	67 80 88	3eqtrd	|- ( ph -> ( ( Q .\/ ( D ` Q ) ) ./\ W ) = ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) )
90	53 89	eqtr2d	|- ( ph -> ( ( ( R ` F ) .\/ U ) ./\ ( ( F ` P ) .\/ V ) ) = ( R ` D ) )
91	41 50 90	3brtr3d	|- ( ph -> V .<_ ( R ` D ) )
92		hlatl	|- ( K e. HL -> K e. AtLat )
93	20 92	syl	|- ( ph -> K e. AtLat )
94		hlop	|- ( K e. HL -> K e. OP )
95	20 94	syl	|- ( ph -> K e. OP )
96		eqid	|- ( 0. ` K ) = ( 0. ` K )
97		eqid	|- ( lt ` K ) = ( lt ` K )
98	96 97 4	0ltat	|- ( ( K e. OP /\ V e. A ) -> ( 0. ` K ) ( lt ` K ) V )
99	95 25 98	syl2anc	|- ( ph -> ( 0. ` K ) ( lt ` K ) V )
100		hlpos	|- ( K e. HL -> K e. Poset )
101	20 100	syl	|- ( ph -> K e. Poset )
102	29 96	op0cl	|- ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
103	95 102	syl	|- ( ph -> ( 0. ` K ) e. ( Base ` K ) )
104	29 5 6 7	trlcl	|- ( ( ( K e. HL /\ W e. H ) /\ D e. T ) -> ( R ` D ) e. ( Base ` K ) )
105	9 18 104	syl2anc	|- ( ph -> ( R ` D ) e. ( Base ` K ) )
106	29 1 97	pltletr	|- ( ( K e. Poset /\ ( ( 0. ` K ) e. ( Base ` K ) /\ V e. ( Base ` K ) /\ ( R ` D ) e. ( Base ` K ) ) ) -> ( ( ( 0. ` K ) ( lt ` K ) V /\ V .<_ ( R ` D ) ) -> ( 0. ` K ) ( lt ` K ) ( R ` D ) ) )
107	101 103 31 105 106	syl13anc	|- ( ph -> ( ( ( 0. ` K ) ( lt ` K ) V /\ V .<_ ( R ` D ) ) -> ( 0. ` K ) ( lt ` K ) ( R ` D ) ) )
108	99 91 107	mp2and	|- ( ph -> ( 0. ` K ) ( lt ` K ) ( R ` D ) )
109	29 97 96	opltn0	|- ( ( K e. OP /\ ( R ` D ) e. ( Base ` K ) ) -> ( ( 0. ` K ) ( lt ` K ) ( R ` D ) <-> ( R ` D ) =/= ( 0. ` K ) ) )
110	95 105 109	syl2anc	|- ( ph -> ( ( 0. ` K ) ( lt ` K ) ( R ` D ) <-> ( R ` D ) =/= ( 0. ` K ) ) )
111	108 110	mpbid	|- ( ph -> ( R ` D ) =/= ( 0. ` K ) )
112	111	neneqd	|- ( ph -> -. ( R ` D ) = ( 0. ` K ) )
113	96 4 5 6 7	trlator0	|- ( ( ( K e. HL /\ W e. H ) /\ D e. T ) -> ( ( R ` D ) e. A \/ ( R ` D ) = ( 0. ` K ) ) )
114	9 18 113	syl2anc	|- ( ph -> ( ( R ` D ) e. A \/ ( R ` D ) = ( 0. ` K ) ) )
115	114	orcomd	|- ( ph -> ( ( R ` D ) = ( 0. ` K ) \/ ( R ` D ) e. A ) )
116	115	ord	|- ( ph -> ( -. ( R ` D ) = ( 0. ` K ) -> ( R ` D ) e. A ) )
117	112 116	mpd	|- ( ph -> ( R ` D ) e. A )
118	1 4	atcmp	|- ( ( K e. AtLat /\ V e. A /\ ( R ` D ) e. A ) -> ( V .<_ ( R ` D ) <-> V = ( R ` D ) ) )
119	93 25 117 118	syl3anc	|- ( ph -> ( V .<_ ( R ` D ) <-> V = ( R ` D ) ) )
120	91 119	mpbid	|- ( ph -> V = ( R ` D ) )
121	120	eqcomd	|- ( ph -> ( R ` D ) = V )