This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ldilset

Description: The set of lattice dilations for a fiducial co-atom W . (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ldilset.b ⊢ B = Base K
ldilset.l ⊢ ≤ ˙ = ≤ K
ldilset.h ⊢ H = LHyp ⁡ K
ldilset.i ⊢ I = LAut ⁡ K
ldilset.d ⊢ D = LDil ⁡ K ⁡ W
Assertion ldilset ⊢ K ∈ C ∧ W ∈ H → D = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x

Proof

Step Hyp Ref Expression
1 ldilset.b ⊢ B = Base K
2 ldilset.l ⊢ ≤ ˙ = ≤ K
3 ldilset.h ⊢ H = LHyp ⁡ K
4 ldilset.i ⊢ I = LAut ⁡ K
5 ldilset.d ⊢ D = LDil ⁡ K ⁡ W
6 1 2 3 4 ldilfset ⊢ K ∈ C → LDil ⁡ K = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
7 6 fveq1d ⊢ K ∈ C → LDil ⁡ K ⁡ W = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x ⁡ W
8 breq2 ⊢ w = W → x ≤ ˙ w ↔ x ≤ ˙ W
9 8 imbi1d ⊢ w = W → x ≤ ˙ w → f ⁡ x = x ↔ x ≤ ˙ W → f ⁡ x = x
10 9 ralbidv ⊢ w = W → ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x ↔ ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x
11 10 rabbidv ⊢ w = W → f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x
12 eqid ⊢ w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
13 4 fvexi ⊢ I ∈ V
14 13 rabex ⊢ f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x ∈ V
15 11 12 14 fvmpt ⊢ W ∈ H → w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x ⁡ W = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x
16 7 15 sylan9eq ⊢ K ∈ C ∧ W ∈ H → LDil ⁡ K ⁡ W = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x
17 5 16 eqtrid ⊢ K ∈ C ∧ W ∈ H → D = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x