Metamath Proof Explorer

Theorem dicelval2nd

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 16-Feb-2014)

Ref Expression
Hypotheses dicelval2nd.l ⊢ ≤ ˙ = ≤ K
dicelval2nd.a ⊢ A = Atoms ⁡ K
dicelval2nd.h ⊢ H = LHyp ⁡ K
dicelval2nd.e ⊢ E = TEndo ⁡ K ⁡ W
dicelval2nd.i ⊢ I = DIsoC ⁡ K ⁡ W
Assertion dicelval2nd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ Y ∈ I ⁡ Q → 2 nd ⁡ Y ∈ E

Proof

Step Hyp Ref Expression
1 dicelval2nd.l ⊢ ≤ ˙ = ≤ K
2 dicelval2nd.a ⊢ A = Atoms ⁡ K
3 dicelval2nd.h ⊢ H = LHyp ⁡ K
4 dicelval2nd.e ⊢ E = TEndo ⁡ K ⁡ W
5 dicelval2nd.i ⊢ I = DIsoC ⁡ K ⁡ W
6 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
7 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
8 1 2 3 5 6 7 dicssdvh ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q ⊆ Base DVecH ⁡ K ⁡ W
9 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
10 3 9 4 6 7 dvhvbase ⊢ K ∈ HL ∧ W ∈ H → Base DVecH ⁡ K ⁡ W = LTrn ⁡ K ⁡ W × E
11 10 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Base DVecH ⁡ K ⁡ W = LTrn ⁡ K ⁡ W × E
12 8 11 sseqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q ⊆ LTrn ⁡ K ⁡ W × E
13 12 sseld ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Y ∈ I ⁡ Q → Y ∈ LTrn ⁡ K ⁡ W × E
14 13 3impia ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ Y ∈ I ⁡ Q → Y ∈ LTrn ⁡ K ⁡ W × E
15 xp2nd ⊢ Y ∈ LTrn ⁡ K ⁡ W × E → 2 nd ⁡ Y ∈ E
16 14 15 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ Y ∈ I ⁡ Q → 2 nd ⁡ Y ∈ E