This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4atlem10b

Description: Lemma for 4at . Substitute V for R (cont.). (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
4at.j ⊢ ∨ = ( join ‘ 𝐾 )
4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4atlem10b ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 4at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 4at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
5 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
6 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
7 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ∈ 𝐴 )
8 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑉 ∈ 𝐴 )
9 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑊 ∈ 𝐴 )
10 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) )
11 1 2 3 4atlem10a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ) → ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
12 6 7 8 9 10 11 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
13 5 12 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
14 4 13 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) )
15 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ∈ 𝐴 )
16 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
17 1 2 3 4atlem9 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ) )
18 6 7 15 9 16 17 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ) )
19 14 18 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) )
20 19 13 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )