Theorem omls 9184

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		eqeq1 1478	. 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		eqeq2 1481	. 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 9066	. . . 4 |- 0H e. CH
5	3, 4	keepel 2395	. . 3 |- if((A (_ B /\ (B i^i (_|_` A)) = 0H), A, 0H) e. CH
6		omls.2	. . . 4 |- B e. SH
7		h0elsh 9067	. . . 4 |- 0H e. SH
8	6, 7	keepel 2395	. . 3 |- if((A (_ B /\ (B i^i (_|_` A)) = 0H), B, 0H) e. SH
9		sseq1 2078	. . . . . 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 3715	. . . . . . . 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 2213	. . . . . . 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	eqeq1d 1480	. . . . . 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 627	. . . . 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 2079	. . . . . 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 2206	. . . . . . 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	eqeq1d 1480	. . . . . 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 627	. . . . 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 2078	. . . . . 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 3715	. . . . . . . 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 2213	. . . . . . 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	eqeq1d 1480	. . . . . 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 627	. . . . 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 2079	. . . . . 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 2206	. . . . . . 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	eqeq1d 1480	. . . . . 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 627	. . . . 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),