Theorem fh2t 9562

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

Assertion

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

Proof of Theorem fh2t

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) /\ (B C_H A /\ B 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) /\ (B C_H A /\ B C_H C)) -> ((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C)))
17		chdmj1t 9452	. . . . . . . . . . . 12 |- (((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))))
18	17, 3, 4	syl2an 454	. . . . . . . . . . 11 |- (((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))))
19		chdmm1t 9448	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
20	19	adantr 389	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
21	20	ineq1d 2216	. . . . . . . . . . 11 |- (((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 i^i C))))
22	18, 21	eqtrd 1507	. . . . . . . . . 10 |- (((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 i^i C))))
23	22	3impdi 880	. . . . . . . . 9 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (_|_` ((A i^i B) vH (A i^i C))) = (((_|_` A) vH (_|_` B)) i^i (_|_` (A i^i C))))
24	23	ineq2d 2217	. . . . . . . 8 |- ((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)))) = ((A i^i (B vH C)) i^i (((_|_` A) vH (_|_` B)) i^i (_|_` (A i^i C)))))
25	24	adantr 389	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B C_H A /\ B C_H C)) -> ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = ((A i^i (B vH C)) i^i (((_|_` A) vH (_|_` B)) i^i (_|_` (A i^i C)))))
26		cmcm2t 9559	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> A C_H (_|_` B)))
27		cmcmt 9557	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> B C_H A))
28		cmbr3t 9551	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ (_|_` B) e. CH) -> (A C_H (_|_` B) <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
29		chocclt 9184	. . . . . . . . . . . . . . 15 |- (B e. CH -> (_|_` B) e. CH)
30	28, 29	sylan2 451	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H (_|_` B) <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
31	26, 27, 30	3bitr3d 548	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (B C_H A <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
32	31	biimpa 416	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ B C_H A) -> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B)))
33		incom 2208	. . . . . . . . . . . 12 |- (A i^i (_|_` B)) = ((_|_` B) i^i A)
34	32, 33	syl6eq 1523	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH) /\ B C_H A) -> (A i^i ((_|_` A) vH (_|_` B))) = ((_|_` B) i^i A))
35	34	3adantl3 805	. . . . . . . . . 10 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ B C_H A) -> (A i^i ((_|_` A) vH (_|_` B))) = ((_|_` B) i^i A))
36	35	adantrr 395	. . . . . . . . 9 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B C_H A /\ B C_H C)) -> (A i^i ((_|_` A) vH (_|_` B))) = ((_|_` B) i^i A))
37	36	ineq1d 2216	. . . . . . . 8 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B C_H A /\ B C_H C)) -> ((A i^i ((_|_` A) vH (_|_` B))) i^i ((B vH C) i^i (_|_` (A i^i C)))) = (((_|_` B) i^i A) i^i ((B vH C) i^i (_|_` (A i^i C)))))
38		in4 2226	. . . . . . . 8 |- ((A i^i (B vH C)) i^i (((_|_` A) vH (_|_` B)) i^i (_|_` (A i^i C)))) = ((A i^i ((_|_` A) vH (_|_` B))) i^i ((B vH C) i^i (_|_` (A i^i C))))
39	37, 38	syl5eq 1519	. . . . . . 7 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B C_H A /\ B C_H C)) -> ((A i^i (B vH C)) i^i (((_|_` A) vH (_|_` B)) i^i (_|_` (A i^i C)))) = (((_|_` B) i^i A) i^i ((B vH C) i^i (_|_` (A i^i C)))))
40	25, 39	eqtrd 1507	. . . . . 6 |- (((A e. CH /\ B e. CH /\ C e. CH) /\ (B C_H A /\ B C_H C)) -> ((A i^i (B vH C)) i^i (_|_` ((A i^i B) vH (A i^i C)))) = (((_|_` B) i^i A) i^i ((B vH C) i^i (_|_` (A i^i C)))))
41		in4 2226	. . . . . 6 |- (((_|_` B) i^i A) i^i (