Theorem fh1t 9561

Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25.

Assertion

Ref	Expression
fh1t	|- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (A i^i (B vH C)) = ((A i^i B) vH (A i^i C)))

Proof of Theorem fh1t

Step	Hyp	Ref	Expression
1		pjomlt 9269	. . 3 |- (((((A i^i B) vH (A i^i C)) e. CH /\ (A i^i (B vH C)) e. SH) /\ (((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C)) /\ ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = 0H)) -> ((A i^i B) vH (A i^i C)) = (A i^i (B vH C)))
2		chjclt 9329	. . . . . . . 8 |- (((A i^i B) e. CH /\ (A i^i C) e. CH) -> ((A i^i B) vH (A i^i C)) e. CH)
3		chinclt 9422	. . . . . . . 8 |- ((A e. CH /\ B e. CH) -> (A i^i B) e. CH)
4		chinclt 9422	. . . . . . . 8 |- ((A e. CH /\ C e. CH) -> (A i^i C) e. CH)
5	2, 3, 4	syl2an 454	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> ((A i^i B) vH (A i^i C)) e. CH)
6	5	anandis 512	. . . . . 6 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> ((A i^i B) vH (A i^i C)) e. CH)
7		chinclt 9422	. . . . . . . 8 |- ((A e. CH /\ (B vH C) e. CH) -> (A i^i (B vH C)) e. CH)
8		chjclt 9329	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
9	7, 8	sylan2 451	. . . . . . 7 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> (A i^i (B vH C)) e. CH)
10		chsh 9096	. . . . . . 7 |- ((A i^i (B vH C)) e. CH -> (A i^i (B vH C)) e. SH)
11	9, 10	syl 10	. . . . . 6 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> (A i^i (B vH C)) e. SH)
12	6, 11	jca 288	. . . . 5 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> (((A i^i B) vH (A i^i C)) e. CH /\ (A i^i (B vH C)) e. SH))
13	12	3impb 829	. . . 4 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (((A i^i B) vH (A i^i C)) e. CH /\ (A i^i (B vH C)) e. SH))
14	13	adantr 389	. . 3 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (((A i^i B) vH (A i^i C)) e. CH /\ (A i^i (B vH C)) e. SH))
15		ledit 9463	. . . . 5 |- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C)))
16	15	adantr 389	. . . 4 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C)))
17		incom 2208	. . . . . . . . 9 |- (A i^i (B vH C)) = ((B vH C) i^i A)
18	17	a1i 8	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (A i^i (B vH C)) = ((B vH C) i^i A))
19		chdmj1t 9452	. . . . . . . . . 10 |- (((A i^i B) e. CH /\ (A i^i C) e. CH) -> (_|_` ((A i^i B) vH (A i^i C))) = ((_|_` (A i^i B)) i^i (_|_` (A i^i C))))
20	19, 3, 4	syl2an 454	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (_|_` ((A i^i B) vH (A i^i C))) = ((_|_` (A i^i B)) i^i (_|_` (A i^i C))))
21		chdmm1t 9448	. . . . . . . . . 10 |- ((A e. CH /\ B e. CH) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
22		chdmm1t 9448	. . . . . . . . . 10 |- ((A e. CH /\ C e. CH) -> (_|_` (A i^i C)) = ((_|_` A) vH (_|_` C)))
23	21, 22	ineqan12d 2219	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> ((_|_` (A i^i B)) i^i (_|_` (A i^i C))) = (((_|_` A) vH (_|_` B)) i^i ((_|_` A) vH (_|_` C))))
24	20, 23	eqtrd 1507	. . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (_|_` ((A i^i B) vH (A i^i C))) = (((_|_` A) vH (_|_` B)) i^i ((_|_` A) vH (_|_` C))))
25	18, 24	ineq12d 2218	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = (((B vH C) i^i A) i^i (((_|_` A) vH (_|_` B)) i^i ((_|_` A) vH (_|_` C)))))
26	25	3impdi 880	. . . . . 6 |- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = (((B vH C) i^i A) i^i (((_|_` A) vH (_|_` B)) i^i ((_|_` A) vH (_|_` C)))))
27	26	adantr 389	. . . . 5 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = (((B vH C) i^i A) i^i (((_|_` A) vH (_|_` B)) i^i ((_|_` A) vH (_|_` C)))))
28		cmcm2t 9559	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> A C_H (_|_` B)))
29		cmbr3t 9551	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ (_|_` B) e. CH) -> (A C_H (_|_` B) <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
30		chocclt 9184	. . . . . . . . . . . . . . 15 |- (B e. CH -> (_|_` B) e. CH)
31	29, 30	sylan2 451	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H (_|_` B) <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
32	28, 31	bitrd 528	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
33	32	biimpa 416	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ A C_H B) -> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B)))
34	33	3adantl3 805	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ A C_H B) -> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B)))
35	34	adantrr 395	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B)))
36		cmcm2t 9559	. . . . . . . . . . . . . 14 |- ((A e. CH /\ C e. CH) -> (A C_H C <-> A C_H (_|_` C)))
37		cmbr3t 9551	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ (_|_` C) e. CH) -> (A C_H (_|_` C) <-> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C))))
38		chocclt 9184	. . . . . . . . . . . . . . 15 |- (C e. CH -> (_|_` C) e. CH)
39	37, 38	sylan2 451	. . . . . . . . . . . . . 14 |- ((A e. CH /\ C e. CH) -> (A C_H (_|_` C) <-> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C))))
40	36, 39	bitrd 528	. . . . . . . . . . . . 13 |- ((A e. CH /\ C e. CH) -> (A C_H C <-> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C))))
41	40	biimpa 416	. . . . . . . . . . . 12 |- (((A e. CH /\ C e. CH) /\ A C_H C) -> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C)))
42	41	3adantl2 804	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ A C_H C) -> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C)))
43	42	adantrl 394	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A C_H B /\ A C_H C)) -> (A i^i ((_|_` A) vH (_|_` C))) = (A i^i (_|_` C))