Theorem fh2t 9557

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 9264	. . 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 9324	. . . . . . . 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 9417	. . . . . . . 8 |- ((A e. CH /\ B e. CH) -> (A i^i B) e. CH)
4		chinclt 9417	. . . . . . . 8 |- ((A e. CH /\ C e. CH) -> (A i^i C) e. CH)
5	2, 3, 4	syl2an 456	. . . . . . 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 514	. . . . . 6 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> ((A i^i B) vH (A i^i C)) e. CH)
7		chinclt 9417	. . . . . . . 8 |- ((A e. CH /\ (B vH C) e. CH) -> (A i^i (B vH C)) e. CH)
8		chjclt 9324	. . . . . . . 8 |- ((B e. CH /\ C e. CH) -> (B vH C) e. CH)
9	7, 8	sylan2 453	. . . . . . 7 |- ((A e. CH /\ (B e. CH /\ C e. CH)) -> (A i^i (B vH C)) e. CH)
10		chsh 9091	. . . . . . 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 831	. . . 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 391	. . 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 9458	. . . . 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 391	. . . 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 9447	. . . . . . . . . . . 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 456	. . . . . . . . . . 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 9443	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
20	19	adantr 391	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ (A e. CH /\ C e. CH)) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
21	20	ineq1d 2219	. . . . . . . . . . 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 1510	. . . . . . . . . 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 882	. . . . . . . . 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 2220	. . . . . . . 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 391	. . . . . . 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 9554	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> A C_H (_|_` B)))
27		cmcmt 9552	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> (A C_H B <-> B C_H A))
28		cmbr3t 9546	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ (_|_` B) e. CH) -> (A C_H (_|_` B) <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
29		chocclt 9179	. . . . . . . . . . . . . . 15 |- (B e. CH -> (_|_` B) e. CH)
30	28, 29	sylan2 453	. . . . . . . . . . . . . 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 550	. . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> (B C_H A <-> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B))))
32	31	biimpa 418	. . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ B C_H A) -> (A i^i ((_|_` A) vH (_|_` B))) = (A i^i (_|_` B)))
33		incom 2211	. . . . . . . . . . . 12 |- (A i^i (_|_` B)) = ((_|_` B) i^i A)
34	32, 33	syl6eq 1526	. . . . . . . . . . 11 |- (((A e. CH /\ B e. CH) /\ B C_H A) -> (A i^i ((_|_` A) vH (_|_` B))) = ((_|_` B) i^i A))
35	34	3adantl3 807	. . . . . . . . . 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 397	. . . . . . . . 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 2219	. . . . . . . 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 2229	. . . . . . . 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 1522	. . . . . . 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 1510	. . . . . 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 2229	. . . . . 6 |- (((_|_` B) i^i A) i^i (