Metamath Proof Explorer


Theorem isltrn2N

Description: The predicate "is a lattice translation". Version of isltrn that considers only different p and q . TODO: Can this eliminate some separate proofs for the p = q case? (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ltrnset.l = ( le ‘ 𝐾 )
ltrnset.j = ( join ‘ 𝐾 )
ltrnset.m = ( meet ‘ 𝐾 )
ltrnset.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnset.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnset.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
ltrnset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion isltrn2N ( ( 𝐾𝐵𝑊𝐻 ) → ( 𝐹𝑇 ↔ ( 𝐹𝐷 ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ltrnset.l = ( le ‘ 𝐾 )
2 ltrnset.j = ( join ‘ 𝐾 )
3 ltrnset.m = ( meet ‘ 𝐾 )
4 ltrnset.a 𝐴 = ( Atoms ‘ 𝐾 )
5 ltrnset.h 𝐻 = ( LHyp ‘ 𝐾 )
6 ltrnset.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
7 ltrnset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 1 2 3 4 5 6 7 isltrn ( ( 𝐾𝐵𝑊𝐻 ) → ( 𝐹𝑇 ↔ ( 𝐹𝐷 ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ) )
9 3simpa ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) )
10 9 imim1i ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
11 3anass ( ( 𝑝𝑞 ∧ ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ↔ ( 𝑝𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) )
12 3anrot ( ( 𝑝𝑞 ∧ ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ↔ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) )
13 df-ne ( 𝑝𝑞 ↔ ¬ 𝑝 = 𝑞 )
14 13 anbi1i ( ( 𝑝𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) )
15 11 12 14 3bitr3i ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) )
16 15 imbi1i ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
17 impexp ( ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
18 16 17 bitri ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
19 id ( 𝑝 = 𝑞𝑝 = 𝑞 )
20 fveq2 ( 𝑝 = 𝑞 → ( 𝐹𝑝 ) = ( 𝐹𝑞 ) )
21 19 20 oveq12d ( 𝑝 = 𝑞 → ( 𝑝 ( 𝐹𝑝 ) ) = ( 𝑞 ( 𝐹𝑞 ) ) )
22 21 oveq1d ( 𝑝 = 𝑞 → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) )
23 22 a1d ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
24 pm2.61 ( ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) → ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
25 23 24 ax-mp ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
26 18 25 sylbi ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
27 10 26 impbii ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
28 27 2ralbii ( ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
29 28 anbi2i ( ( 𝐹𝐷 ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ↔ ( 𝐹𝐷 ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
30 8 29 bitrdi ( ( 𝐾𝐵𝑊𝐻 ) → ( 𝐹𝑇 ↔ ( 𝐹𝐷 ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝑝𝑞 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ) )