Metamath Proof Explorer


Theorem 4atlem12a

Description: Lemma for 4at . Substitute T for P . (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l = ( le ‘ 𝐾 )
4at.j = ( join ‘ 𝐾 )
4at.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4atlem12a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l = ( le ‘ 𝐾 )
2 4at.j = ( join ‘ 𝐾 )
3 4at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝐾 ∈ HL )
5 simp12 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑃𝐴 )
6 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑇𝐴 )
7 4 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝐾 ∈ Lat )
8 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑈𝐴 )
9 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑉𝐴 )
10 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴 ) → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
12 4 8 9 11 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
13 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑊𝐴 )
14 10 3 atbase ( 𝑊𝐴𝑊 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16 10 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑈 𝑉 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
17 7 12 15 16 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( ( 𝑈 𝑉 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
18 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) )
19 10 1 2 3 hlexchb2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑇𝐴 ∧ ( ( 𝑈 𝑉 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ↔ ( 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) = ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ) )
20 4 5 6 17 18 19 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ↔ ( 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) = ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ) )
21 1 2 3 4atlem4a ( ( ( 𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴 ) ∧ ( 𝑉𝐴𝑊𝐴 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) = ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) )
22 4 6 8 9 13 21 syl32anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) = ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) )
23 22 breq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ 𝑃 ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ) )
24 1 2 3 4atlem4a ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴 ) ∧ ( 𝑉𝐴𝑊𝐴 ) ) → ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) )
25 4 5 8 9 13 24 syl32anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) )
26 25 22 eqeq12d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) = ( 𝑇 ( ( 𝑈 𝑉 ) 𝑊 ) ) ) )
27 20 23 26 3bitr4d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴 ) ∧ ( 𝑈𝐴𝑉𝐴𝑊𝐴 ) ∧ ¬ 𝑃 ( ( 𝑈 𝑉 ) 𝑊 ) ) → ( 𝑃 ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ↔ ( ( 𝑃 𝑈 ) ( 𝑉 𝑊 ) ) = ( ( 𝑇 𝑈 ) ( 𝑉 𝑊 ) ) ) )