Metamath Proof Explorer

Theorem dicfval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013)

Ref Expression
Hypotheses dicval.l ⊢ ≤ ˙ = ≤ K
dicval.a ⊢ A = Atoms ⁡ K
dicval.h ⊢ H = LHyp ⁡ K
dicval.p ⊢ P = oc ⁡ K ⁡ W
dicval.t ⊢ T = LTrn ⁡ K ⁡ W
dicval.e ⊢ E = TEndo ⁡ K ⁡ W
dicval.i ⊢ I = DIsoC ⁡ K ⁡ W
Assertion dicfval ⊢ K ∈ V ∧ W ∈ H → I = q ∈ r ∈ A | ¬ r ≤ ˙ W ⟼ f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E

Proof

Step Hyp Ref Expression
1 dicval.l ⊢ ≤ ˙ = ≤ K
2 dicval.a ⊢ A = Atoms ⁡ K
3 dicval.h ⊢ H = LHyp ⁡ K
4 dicval.p ⊢ P = oc ⁡ K ⁡ W
5 dicval.t ⊢ T = LTrn ⁡ K ⁡ W
6 dicval.e ⊢ E = TEndo ⁡ K ⁡ W
7 dicval.i ⊢ I = DIsoC ⁡ K ⁡ W
8 1 2 3 dicffval ⊢ K ∈ V → DIsoC ⁡ K = w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w
9 8 fveq1d ⊢ K ∈ V → DIsoC ⁡ K ⁡ W = w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w ⁡ W
10 7 9 syl5eq ⊢ K ∈ V → I = w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w ⁡ W
11 breq2 ⊢ w = W → r ≤ ˙ w ↔ r ≤ ˙ W
12 11 notbid ⊢ w = W → ¬ r ≤ ˙ w ↔ ¬ r ≤ ˙ W
13 12 rabbidv ⊢ w = W → r ∈ A | ¬ r ≤ ˙ w = r ∈ A | ¬ r ≤ ˙ W
14 fveq2 ⊢ w = W → LTrn ⁡ K ⁡ w = LTrn ⁡ K ⁡ W
15 14 5 eqtr4di ⊢ w = W → LTrn ⁡ K ⁡ w = T
16 fveq2 ⊢ w = W → oc ⁡ K ⁡ w = oc ⁡ K ⁡ W
17 16 4 eqtr4di ⊢ w = W → oc ⁡ K ⁡ w = P
18 17 fveqeq2d ⊢ w = W → g ⁡ oc ⁡ K ⁡ w = q ↔ g ⁡ P = q
19 15 18 riotaeqbidv ⊢ w = W → ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q = ι g ∈ T | g ⁡ P = q
20 19 fveq2d ⊢ w = W → s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q = s ⁡ ι g ∈ T | g ⁡ P = q
21 20 eqeq2d ⊢ w = W → f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ↔ f = s ⁡ ι g ∈ T | g ⁡ P = q
22 fveq2 ⊢ w = W → TEndo ⁡ K ⁡ w = TEndo ⁡ K ⁡ W
23 22 6 eqtr4di ⊢ w = W → TEndo ⁡ K ⁡ w = E
24 23 eleq2d ⊢ w = W → s ∈ TEndo ⁡ K ⁡ w ↔ s ∈ E
25 21 24 anbi12d ⊢ w = W → f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w ↔ f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E
26 25 opabbidv ⊢ w = W → f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w = f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E
27 13 26 mpteq12dv ⊢ w = W → q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w = q ∈ r ∈ A | ¬ r ≤ ˙ W ⟼ f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E
28 eqid ⊢ w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w = w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w
29 2 fvexi ⊢ A ∈ V
30 29 mptrabex ⊢ q ∈ r ∈ A | ¬ r ≤ ˙ W ⟼ f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E ∈ V
31 27 28 30 fvmpt ⊢ W ∈ H → w ∈ H ⟼ q ∈ r ∈ A | ¬ r ≤ ˙ w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ w | g ⁡ oc ⁡ K ⁡ w = q ∧ s ∈ TEndo ⁡ K ⁡ w ⁡ W = q ∈ r ∈ A | ¬ r ≤ ˙ W ⟼ f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E
32 10 31 sylan9eq ⊢ K ∈ V ∧ W ∈ H → I = q ∈ r ∈ A | ¬ r ≤ ˙ W ⟼ f s | f = s ⁡ ι g ∈ T | g ⁡ P = q ∧ s ∈ E