Theorem omls 5251

Description: Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22.

Hypotheses

Ref	Expression
omls.1	|- A e. CH
omls.2	|- B e. SH

Assertion

Ref	Expression
omls	|- ((A (_ B /\ (B i^i (_|_` A)) = 0H) -> A = B)

Proof of Theorem omls

Step	Hyp	Ref	Expression
1		cleq1 1107	. 2 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (A = B <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) = B))
2		cleq2 1110	. 2 |- (B = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) = B <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H)))
3		omls.1	. . . 4 |- A e. CH
4		h0elch 5159	. . . 4 |- 0H e. CH
5	3, 4	keepel 1796	. . 3 |- if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) e. CH
6		omls.2	. . . 4 |- B e. SH
7	4	chshi 5132	. . . 4 |- 0H e. SH
8	6, 7	keepel 1796	. . 3 |- if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) e. SH
9		sseq1 1521	. . . . . 6 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (A (_ B <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ B))
10		fveq2 2832	. . . . . . . 8 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (_|_` A) = (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H)))
11	10	ineq2d 1645	. . . . . . 7 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (B i^i (_|_` A)) = (B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))))
12	11	cleq1d 1109	. . . . . 6 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> ((B i^i (_|_` A)) = 0H <-> (B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H))
13	9, 12	anbi12d 476	. . . . 5 |- (A = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> ((A (_ B /\ (B i^i (_|_` A)) = 0H) <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ B /\ (B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H)))
14		sseq2 1522	. . . . . 6 |- (B = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ B <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H)))
15		ineq1 1638	. . . . . . 7 |- (B = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> (B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))))
16	15	cleq1d 1109	. . . . . 6 |- (B = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> ((B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H))
17	14, 16	anbi12d 476	. . . . 5 |- (B = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> ((if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ B /\ (B i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H) <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) /\ (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H)))
18		sseq1 1521	. . . . . 6 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (0H (_ 0H <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ 0H))
19		fveq2 2832	. . . . . . . 8 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (_|_` 0H) = (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H)))
20	19	ineq2d 1645	. . . . . . 7 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> (0H i^i (_|_` 0H)) = (0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))))
21	20	cleq1d 1109	. . . . . 6 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> ((0H i^i (_|_` 0H)) = 0H <-> (0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H))
22	18, 21	anbi12d 476	. . . . 5 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) -> ((0H (_ 0H /\ (0H i^i (_|_` 0H)) = 0H) <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ 0H /\ (0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H)))
23		sseq2 1522	. . . . . 6 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ 0H <-> if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H)))
24		ineq1 1638	. . . . . . 7 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> (0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))))
25	24	cleq1d 1109	. . . . . 6 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> ((0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H))
26	23, 25	anbi12d 476	. . . . 5 |- (0H = if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) -> ((if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ 0H /\ (0H i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H) <-> (if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) (_ if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) /\ (if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) i^i (_|_` if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H))) = 0H)))
27		ssid 1519	. . . . . 6 |- 0H (_ 0H
28		ocin 5177	. . . . . . 7 |- (0H e. SH ->