Metamath Proof Explorer

Theorem trlval2

Description: The value of the trace of a lattice translation, given any atom P not under the fiducial co-atom W . Note: this requires only the weaker assumption K e. Lat ; we use K e. HL for convenience. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses trlval2.l ⊢ ≤ = ( le ‘ 𝐾 )
trlval2.j ⊢ ∨ = ( join ‘ 𝐾 )
trlval2.m ⊢ ∧ = ( meet ‘ 𝐾 )
trlval2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trlval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trlval2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trlval2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trlval2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 trlval2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 trlval2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 trlval2.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 trlval2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 trlval2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 trlval2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 trlval2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 8 anim1i ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 1 2 3 4 5 6 7 trlval ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
12 11 3adant3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
13 simp1l ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
14 simp3l ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
15 10 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
17 10 5 6 ltrncl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
18 16 17 syld3an3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
19 10 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
20 13 16 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
21 simp1r ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
22 10 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
24 10 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
25 13 20 23 24 syl3anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
26 simpl3l ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ∈ 𝐴 )
27 simpl3r ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ¬ 𝑃 ≤ 𝑊 )
28 breq1 ⊢ ( 𝑞 = 𝑃 → ( 𝑞 ≤ 𝑊 ↔ 𝑃 ≤ 𝑊 ) )
29 28 notbid ⊢ ( 𝑞 = 𝑃 → ( ¬ 𝑞 ≤ 𝑊 ↔ ¬ 𝑃 ≤ 𝑊 ) )
30 id ⊢ ( 𝑞 = 𝑃 → 𝑞 = 𝑃 )
31 fveq2 ⊢ ( 𝑞 = 𝑃 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑃 ) )
32 30 31 oveq12d ⊢ ( 𝑞 = 𝑃 → ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
33 32 oveq1d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
34 33 eqeq2d ⊢ ( 𝑞 = 𝑃 → ( 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ↔ 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
35 29 34 imbi12d ⊢ ( 𝑞 = 𝑃 → ( ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑃 ≤ 𝑊 → 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) ) )
36 35 rspcv ⊢ ( 𝑃 ∈ 𝐴 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → ( ¬ 𝑃 ≤ 𝑊 → 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) ) )
37 36 com23 ⊢ ( 𝑃 ∈ 𝐴 → ( ¬ 𝑃 ≤ 𝑊 → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) ) )
38 26 27 37 sylc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
39 simp11 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) )
40 simp12 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → 𝐹 ∈ 𝑇 )
41 simp13l ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
42 simp13r ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → ¬ 𝑃 ≤ 𝑊 )
43 simp3 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
44 simp2 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → ¬ 𝑞 ≤ 𝑊 )
45 1 2 3 4 5 6 ltrnu ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) )
46 39 40 41 42 43 44 45 syl222anc ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) )
47 eqeq2 ⊢ ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ↔ 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
48 47 biimpd ⊢ ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
49 46 48 syl ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
50 49 3exp ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ¬ 𝑞 ≤ 𝑊 → ( 𝑞 ∈ 𝐴 → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )
51 50 com24 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → ( 𝑞 ∈ 𝐴 → ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )
52 51 ralrimdv ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
53 52 adantr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) → ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
54 38 53 impbid ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ 𝑥 = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ) )
55 25 54 riota5 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 → 𝑥 = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
56 12 55 eqtrd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
57 9 56 syl3an1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )