Metamath Proof Explorer

Theorem dicopelval2

Description: Membership in value of 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
dicelval2.f ⊢ F ∈ V
dicelval2.s ⊢ S ∈ V
Assertion dicopelval2 ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ 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 dicelval2.f ⊢ F ∈ V
10 dicelval2.s ⊢ S ∈ V
11 1 2 3 4 5 6 7 9 10 dicopelval ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q ∧ S ∈ E
12 8 fveq2i ⊢ S ⁡ G = S ⁡ ι g ∈ T | g ⁡ P = Q
13 12 eqeq2i ⊢ F = S ⁡ G ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q
14 13 anbi1i ⊢ F = S ⁡ G ∧ S ∈ E ↔ F = S ⁡ ι g ∈ T | g ⁡ P = Q ∧ S ∈ E
15 11 14 bitr4di ⊢ K ∈ V ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F S ∈ I ⁡ Q ↔ F = S ⁡ G ∧ S ∈ E