Metamath Proof Explorer

Theorem dicval2

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 20-Feb-2014)

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
dicval2.g ⊢ G = ι g ∈ T | g ⁡ P = Q
Assertion dicval2 ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = f s | f = s ⁡ G ∧ 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 dicval2.g ⊢ G = ι g ∈ T | g ⁡ P = Q
9 1 2 3 4 5 6 7 dicval ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = f s | f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E
10 8 fveq2i ⊢ s ⁡ G = s ⁡ ι g ∈ T | g ⁡ P = Q
11 10 eqeq2i ⊢ f = s ⁡ G ↔ f = s ⁡ ι g ∈ T | g ⁡ P = Q
12 11 anbi1i ⊢ f = s ⁡ G ∧ s ∈ E ↔ f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E
13 12 opabbii ⊢ f s | f = s ⁡ G ∧ s ∈ E = f s | f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E
14 9 13 eqtr4di ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = f s | f = s ⁡ G ∧ s ∈ E