Metamath Proof Explorer

Theorem ldilfset

Description: The mapping from fiducial co-atom w to its set of lattice dilations. (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
Assertion ldilfset ⊢ K ∈ C → LDil ⁡ K = w ∈ H ⟼ 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 elex ⊢ K ∈ C → K ∈ V
6 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
7 6 3 eqtr4di ⊢ k = K → LHyp ⁡ k = H
8 fveq2 ⊢ k = K → LAut ⁡ k = LAut ⁡ K
9 8 4 eqtr4di ⊢ k = K → LAut ⁡ k = I
10 fveq2 ⊢ k = K → Base k = Base K
11 10 1 eqtr4di ⊢ k = K → Base k = B
12 fveq2 ⊢ k = K → ≤ k = ≤ K
13 12 2 eqtr4di ⊢ k = K → ≤ k = ≤ ˙
14 13 breqd ⊢ k = K → x ≤ k w ↔ x ≤ ˙ w
15 14 imbi1d ⊢ k = K → x ≤ k w → f ⁡ x = x ↔ x ≤ ˙ w → f ⁡ x = x
16 11 15 raleqbidv ⊢ k = K → ∀ x ∈ Base k x ≤ k w → f ⁡ x = x ↔ ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
17 9 16 rabeqbidv ⊢ k = K → f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x = f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
18 7 17 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
19 df-ldil ⊢ LDil = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LAut ⁡ k | ∀ x ∈ Base k x ≤ k w → f ⁡ x = x
20 18 19 3 mptfvmpt ⊢ K ∈ V → LDil ⁡ K = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x
21 5 20 syl ⊢ K ∈ C → LDil ⁡ K = w ∈ H ⟼ f ∈ I | ∀ x ∈ B x ≤ ˙ w → f ⁡ x = x