Metamath Proof Explorer

Theorem ldilcnv

Description: The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013)

Ref Expression
Hypotheses ldilcnv.h ⊢ H = LHyp ⁡ K
ldilcnv.d ⊢ D = LDil ⁡ K ⁡ W
Assertion ldilcnv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F -1 ∈ D

Proof

Step Hyp Ref Expression
1 ldilcnv.h ⊢ H = LHyp ⁡ K
2 ldilcnv.d ⊢ D = LDil ⁡ K ⁡ W
3 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → K ∈ HL
4 eqid ⊢ LAut ⁡ K = LAut ⁡ K
5 1 4 2 ldillaut ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F ∈ LAut ⁡ K
6 4 lautcnv ⊢ K ∈ HL ∧ F ∈ LAut ⁡ K → F -1 ∈ LAut ⁡ K
7 3 5 6 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F -1 ∈ LAut ⁡ K
8 eqid ⊢ Base K = Base K
9 eqid ⊢ ≤ K = ≤ K
10 8 9 1 2 ldilval ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F ⁡ x = x
11 10 3expa ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F ⁡ x = x
12 11 3impb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F ⁡ x = x
13 12 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F -1 ⁡ F ⁡ x = F -1 ⁡ x
14 8 1 2 ldil1o ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F : Base K ⟶ 1-1 onto Base K
15 14 3ad2ant1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F : Base K ⟶ 1-1 onto Base K
16 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → x ∈ Base K
17 f1ocnvfv1 ⊢ F : Base K ⟶ 1-1 onto Base K ∧ x ∈ Base K → F -1 ⁡ F ⁡ x = x
18 15 16 17 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F -1 ⁡ F ⁡ x = x
19 13 18 eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D ∧ x ∈ Base K ∧ x ≤ K W → F -1 ⁡ x = x
20 19 3exp ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → x ∈ Base K → x ≤ K W → F -1 ⁡ x = x
21 20 ralrimiv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → ∀ x ∈ Base K x ≤ K W → F -1 ⁡ x = x
22 8 9 1 4 2 isldil ⊢ K ∈ HL ∧ W ∈ H → F -1 ∈ D ↔ F -1 ∈ LAut ⁡ K ∧ ∀ x ∈ Base K x ≤ K W → F -1 ⁡ x = x
23 22 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F -1 ∈ D ↔ F -1 ∈ LAut ⁡ K ∧ ∀ x ∈ Base K x ≤ K W → F -1 ⁡ x = x
24 7 21 23 mpbir2and ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ D → F -1 ∈ D