Metamath Proof Explorer

Theorem dicopelval

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 15-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
dicelval.f ⊢ F ∈ V
dicelval.s ⊢ S ∈ V
Assertion dicopelval ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ 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 dicelval.f ⊢ F ∈ V
9 dicelval.s ⊢ S ∈ V
10 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
11 10 eleq2d ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F S ∈ f s | f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E
12 eqeq1 ⊢ f = F → f = s ⁡ ι g ∈ T | g ⁡ P = Q ↔ F = s ⁡ ι g ∈ T | g ⁡ P = Q
13 12 anbi1d ⊢ f = F → f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E ↔ F = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E
14 fveq1 ⊢ s = S → s ⁡ ι g ∈ T | g ⁡ P = Q = S ⁡ ι g ∈ T | g ⁡ P = Q
15 14 eqeq2d ⊢ s = S → F = s ⁡ ι g ∈ T | g ⁡ P = Q ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q
16 eleq1 ⊢ s = S → s ∈ E ↔ S ∈ E
17 15 16 anbi12d ⊢ s = S → F = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q ∧ S ∈ E
18 8 9 13 17 opelopab ⊢ F S ∈ f s | f = s ⁡ ι g ∈ T | g ⁡ P = Q ∧ s ∈ E ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q ∧ S ∈ E
19 11 18 bitrdi ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q ∧ S ∈ E