omlfh1N

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omlfh1.b	\|- B = ( Base ` K )
	omlfh1.j	\|- .\/ = ( join ` K )
	omlfh1.m	\|- ./\ = ( meet ` K )
	omlfh1.c	\|- C = ( cm ` K )
Assertion	omlfh1N	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		omlfh1.b	\|- B = ( Base ` K )
2		omlfh1.j	\|- .\/ = ( join ` K )
3		omlfh1.m	\|- ./\ = ( meet ` K )
4		omlfh1.c	\|- C = ( cm ` K )
5		omllat	\|- ( K e. OML -> K e. Lat )
6		eqid	\|- ( le ` K ) = ( le ` K )
7	1 6 2 3	latledi	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
8	5 7	sylan	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
9	8	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) )
10	5	adantr	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
11		simpr1	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
12		simpr2	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
13		simpr3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
14	1 2	latjcl	\|- ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y .\/ Z ) e. B )
15	10 12 13 14	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) e. B )
16	1 3	latmcom	\|- ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) ./\ X ) )
17	10 11 15 16	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) ./\ X ) )
18		omlol	\|- ( K e. OML -> K e. OL )
19	18	adantr	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OL )
20	1 3	latmcl	\|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
21	10 11 12 20	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) e. B )
22	1 3	latmcl	\|- ( ( K e. Lat /\ X e. B /\ Z e. B ) -> ( X ./\ Z ) e. B )
23	10 11 13 22	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Z ) e. B )
24		eqid	\|- ( oc ` K ) = ( oc ` K )
25	1 2 3 24	oldmj1	\|- ( ( K e. OL /\ ( X ./\ Y ) e. B /\ ( X ./\ Z ) e. B ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) )
26	19 21 23 25	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) )
27	1 2 3 24	oldmm1	\|- ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( X ./\ Y ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) )
28	19 11 12 27	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( X ./\ Y ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) )
29	1 2 3 24	oldmm1	\|- ( ( K e. OL /\ X e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( X ./\ Z ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) )
30	19 11 13 29	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( X ./\ Z ) ) = ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) )
31	28 30	oveq12d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` ( X ./\ Y ) ) ./\ ( ( oc ` K ) ` ( X ./\ Z ) ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) )
32	26 31	eqtrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) = ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) )
33	17 32	oveq12d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
34	33	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
35		omlop	\|- ( K e. OML -> K e. OP )
36	35	adantr	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OP )
37	1 24	opoccl	\|- ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
38	36 11 37	syl2anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` X ) e. B )
39	1 24	opoccl	\|- ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
40	36 12 39	syl2anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Y ) e. B )
41	1 2	latjcl	\|- ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B )
42	10 38 40 41	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B )
43	1 24	opoccl	\|- ( ( K e. OP /\ Z e. B ) -> ( ( oc ` K ) ` Z ) e. B )
44	36 13 43	syl2anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Z ) e. B )
45	1 2	latjcl	\|- ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B )
46	10 38 44 45	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B )
47	1 3	latmcl	\|- ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B )
48	10 42 46 47	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B )
49	1 3	latmassOLD	\|- ( ( K e. OL /\ ( ( Y .\/ Z ) e. B /\ X e. B /\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) e. B ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
50	19 15 11 48 49	syl13anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
51	50	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) )
52	1 24 4	cmt2N	\|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> X C ( ( oc ` K ) ` Y ) ) )
53	52	3adant3r3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y <-> X C ( ( oc ` K ) ` Y ) ) )
54		simpl	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OML )
55	1 2 3 24 4	cmtbr3N	\|- ( ( K e. OML /\ X e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( X C ( ( oc ` K ) ` Y ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
56	54 11 40 55	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C ( ( oc ` K ) ` Y ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
57	53 56	bitrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) ) )
58	57	biimpa	\|- ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
59	58	adantrr	\|- ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
60	59	3impa	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) = ( X ./\ ( ( oc ` K ) ` Y ) ) )
61	1 24 4	cmt2N	\|- ( ( K e. OML /\ X e. B /\ Z e. B ) -> ( X C Z <-> X C ( ( oc ` K ) ` Z ) ) )
62	61	3adant3r2	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Z <-> X C ( ( oc ` K ) ` Z ) ) )
63	1 2 3 24 4	cmtbr3N	\|- ( ( K e. OML /\ X e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( X C ( ( oc ` K ) ` Z ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
64	54 11 44 63	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C ( ( oc ` K ) ` Z ) <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
65	62 64	bitrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Z <-> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
66	65	biimpa	\|- ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Z ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
67	66	adantrl	\|- ( ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
68	67	3impa	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) = ( X ./\ ( ( oc ` K ) ` Z ) ) )
69	60 68	oveq12d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
70	1 3	latmmdiN	\|- ( ( K e. OL /\ ( X e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) e. B /\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) e. B ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
71	19 11 42 46 70	syl13anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
72	71	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ) ./\ ( X ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) )
73	1 3	latmmdiN	\|- ( ( K e. OL /\ ( X e. B /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
74	19 11 40 44 73	syl13anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
75	74	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( ( X ./\ ( ( oc ` K ) ` Y ) ) ./\ ( X ./\ ( ( oc ` K ) ` Z ) ) ) )
76	69 72 75	3eqtr4d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) )
77	76	oveq2d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) ) = ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
78	1 3	latmcl	\|- ( ( K e. Lat /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B )
79	10 40 44 78	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B )
80	1 3	latm12	\|- ( ( K e. OL /\ ( ( Y .\/ Z ) e. B /\ X e. B /\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) e. B ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
81	19 15 11 79 80	syl13anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
82	81	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( Y .\/ Z ) ./\ ( X ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
83	51 77 82	3eqtrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( Y .\/ Z ) ./\ X ) ./\ ( ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Y ) ) ./\ ( ( ( oc ` K ) ` X ) .\/ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) )
84	1 2 3 24	oldmj1	\|- ( ( K e. OL /\ Y e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( Y .\/ Z ) ) = ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) )
85	19 12 13 84	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( Y .\/ Z ) ) = ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) )
86	85	oveq2d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) )
87		eqid	\|- ( 0. ` K ) = ( 0. ` K )
88	1 24 3 87	opnoncon	\|- ( ( K e. OP /\ ( Y .\/ Z ) e. B ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( 0. ` K ) )
89	36 15 88	syl2anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( oc ` K ) ` ( Y .\/ Z ) ) ) = ( 0. ` K ) )
90	86 89	eqtr3d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) = ( 0. ` K ) )
91	90	oveq2d	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( 0. ` K ) ) )
92	1 3 87	olm01	\|- ( ( K e. OL /\ X e. B ) -> ( X ./\ ( 0. ` K ) ) = ( 0. ` K ) )
93	19 11 92	syl2anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( 0. ` K ) ) = ( 0. ` K ) )
94	91 93	eqtrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( 0. ` K ) )
95	94	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( ( Y .\/ Z ) ./\ ( ( ( oc ` K ) ` Y ) ./\ ( ( oc ` K ) ` Z ) ) ) ) = ( 0. ` K ) )
96	34 83 95	3eqtrd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) )
97	1 2	latjcl	\|- ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ ( X ./\ Z ) e. B ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B )
98	10 21 23 97	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B )
99	1 3	latmcl	\|- ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X ./\ ( Y .\/ Z ) ) e. B )
100	10 11 15 99	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y .\/ Z ) ) e. B )
101	1 6 3 24 87	omllaw3	\|- ( ( K e. OML /\ ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) e. B /\ ( X ./\ ( Y .\/ Z ) ) e. B ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
102	54 98 100 101	syl3anc	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
103	102	3adant3	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ( le ` K ) ( X ./\ ( Y .\/ Z ) ) /\ ( ( X ./\ ( Y .\/ Z ) ) ./\ ( ( oc ` K ) ` ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) ) = ( 0. ` K ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) ) )
104	9 96 103	mp2and	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) = ( X ./\ ( Y .\/ Z ) ) )
105	104	eqcomd	\|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )

Metamath Proof Explorer

Theorem omlfh1N

Proof