Metamath Proof Explorer


Theorem 3dimlem3a

Description: Lemma for 3dim3 . (Contributed by NM, 27-Jul-2012)

Ref Expression
Hypotheses 3dim0.j = ( join ‘ 𝐾 )
3dim0.l = ( le ‘ 𝐾 )
3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dimlem3a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 3dim0.j = ( join ‘ 𝐾 )
2 3dim0.l = ( le ‘ 𝐾 )
3 3dim0.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) )
5 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝐾 ∈ HL )
6 5 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝐾 ∈ Lat )
7 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑄𝐴 )
8 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
10 7 9 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
11 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑅𝐴 )
12 8 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
13 11 12 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
14 simp12 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑃𝐴 )
15 8 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
17 8 1 latjrot ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
18 6 10 13 16 17 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
19 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) )
20 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → 𝑆𝐴 )
21 8 1 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
22 5 7 11 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
23 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
24 8 2 1 3 hlexchb1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑆𝐴 ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ↔ ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑄 𝑅 ) 𝑆 ) ) )
25 5 14 20 22 23 24 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ↔ ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑄 𝑅 ) 𝑆 ) ) )
26 19 25 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑄 𝑅 ) 𝑆 ) )
27 18 26 eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑄 𝑅 ) 𝑆 ) )
28 27 breq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ( 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ) )
29 4 28 mtbird ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( ¬ 𝑇 ( ( 𝑄 𝑅 ) 𝑆 ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) ) → ¬ 𝑇 ( ( 𝑃 𝑄 ) 𝑅 ) )