Theorem pjoml3i

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	⊢ 𝐴 ∈ Cℋ
	pjoml2.2	⊢ 𝐵 ∈ Cℋ
Assertion	pjoml3i	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	⊢ 𝐴 ∈ Cℋ
2		pjoml2.2	⊢ 𝐵 ∈ Cℋ
3	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
5	3 4	pjoml2i	⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
6	2 1	chsscon3i	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝐵 ) )
7		eqcom	⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = 𝐵 ↔ 𝐵 = ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
8	3	choccli	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ
9	8 4	chincli	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
10	1 9	chdmj2i	⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) )
11	3 2	chdmm4i	⊢ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
12	11	ineq2i	⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
13	10 12	eqtri	⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
14	13	eqeq1i	⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )
15	3 9	chjcli	⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
16	2 15	chcon2i	⊢ ( 𝐵 = ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
17	7 14 16	3bitr3i	⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 ↔ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
18	5 6 17	3imtr4i	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )