omlsilem

Description: Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omlsilem.1	⊢ 𝐺 ∈ S_ℋ
	omlsilem.2	⊢ 𝐻 ∈ S_ℋ
	omlsilem.3	⊢ 𝐺 ⊆ 𝐻
	omlsilem.4	⊢ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) = 0_ℋ
	omlsilem.5	⊢ 𝐴 ∈ 𝐻
	omlsilem.6	⊢ 𝐵 ∈ 𝐺
	omlsilem.7	⊢ 𝐶 ∈ ( ⊥ ‘ 𝐺 )
Assertion	omlsilem	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → 𝐴 ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		omlsilem.1	⊢ 𝐺 ∈ S_ℋ
2		omlsilem.2	⊢ 𝐻 ∈ S_ℋ
3		omlsilem.3	⊢ 𝐺 ⊆ 𝐻
4		omlsilem.4	⊢ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) = 0_ℋ
5		omlsilem.5	⊢ 𝐴 ∈ 𝐻
6		omlsilem.6	⊢ 𝐵 ∈ 𝐺
7		omlsilem.7	⊢ 𝐶 ∈ ( ⊥ ‘ 𝐺 )
8	2 5	shelii	⊢ 𝐴 ∈ ℋ
9	1 6	shelii	⊢ 𝐵 ∈ ℋ
10		shocss	⊢ ( 𝐺 ∈ S_ℋ → ( ⊥ ‘ 𝐺 ) ⊆ ℋ )
11	1 10	ax-mp	⊢ ( ⊥ ‘ 𝐺 ) ⊆ ℋ
12	11 7	sselii	⊢ 𝐶 ∈ ℋ
13	8 9 12	hvsubaddi	⊢ ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +_ℎ 𝐶 ) = 𝐴 )
14		eqcom	⊢ ( ( 𝐵 +_ℎ 𝐶 ) = 𝐴 ↔ 𝐴 = ( 𝐵 +_ℎ 𝐶 ) )
15	13 14	bitri	⊢ ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 ↔ 𝐴 = ( 𝐵 +_ℎ 𝐶 ) )
16	3 6	sselii	⊢ 𝐵 ∈ 𝐻
17		shsubcl	⊢ ( ( 𝐻 ∈ S_ℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −_ℎ 𝐵 ) ∈ 𝐻 )
18	2 5 16 17	mp3an	⊢ ( 𝐴 −_ℎ 𝐵 ) ∈ 𝐻
19		eleq1	⊢ ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 → ( ( 𝐴 −_ℎ 𝐵 ) ∈ 𝐻 ↔ 𝐶 ∈ 𝐻 ) )
20	18 19	mpbii	⊢ ( ( 𝐴 −_ℎ 𝐵 ) = 𝐶 → 𝐶 ∈ 𝐻 )
21	15 20	sylbir	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → 𝐶 ∈ 𝐻 )
22	4	eleq2i	⊢ ( 𝐶 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ↔ 𝐶 ∈ 0_ℋ )
23		elin	⊢ ( 𝐶 ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐺 ) ) ↔ ( 𝐶 ∈ 𝐻 ∧ 𝐶 ∈ ( ⊥ ‘ 𝐺 ) ) )
24		elch0	⊢ ( 𝐶 ∈ 0_ℋ ↔ 𝐶 = 0_ℎ )
25	22 23 24	3bitr3i	⊢ ( ( 𝐶 ∈ 𝐻 ∧ 𝐶 ∈ ( ⊥ ‘ 𝐺 ) ) ↔ 𝐶 = 0_ℎ )
26	21 7 25	sylanblc	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → 𝐶 = 0_ℎ )
27	26	oveq2d	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → ( 𝐵 +_ℎ 𝐶 ) = ( 𝐵 +_ℎ 0_ℎ ) )
28		ax-hvaddid	⊢ ( 𝐵 ∈ ℋ → ( 𝐵 +_ℎ 0_ℎ ) = 𝐵 )
29	9 28	ax-mp	⊢ ( 𝐵 +_ℎ 0_ℎ ) = 𝐵
30	27 29	eqtrdi	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → ( 𝐵 +_ℎ 𝐶 ) = 𝐵 )
31	30 6	eqeltrdi	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → ( 𝐵 +_ℎ 𝐶 ) ∈ 𝐺 )
32		eleq1	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → ( 𝐴 ∈ 𝐺 ↔ ( 𝐵 +_ℎ 𝐶 ) ∈ 𝐺 ) )
33	31 32	mpbird	⊢ ( 𝐴 = ( 𝐵 +_ℎ 𝐶 ) → 𝐴 ∈ 𝐺 )

Metamath Proof Explorer

Theorem omlsilem

Proof