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 ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑉𝐴 ) ∧ ( 𝑊𝐴 ∧ ¬ 𝑅 ( ( 𝑃 𝑄 ) 𝑊 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) ∧ ( 𝑅 ( ( 𝑃 𝑄 ) ( 𝑉 𝑊 ) ) ∧ 𝑆 ( ( 𝑃 𝑄 ) ( 𝑉 𝑊 ) ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑅 𝑆 ) ) = ( ( 𝑃 𝑄 ) ( 𝑉 𝑊 ) ) )