Metamath Proof Explorer

Theorem dihopelvalc

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dihopelvalcp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihopelvalcp.l ⊢ ≤ = ( le ‘ 𝐾 )
dihopelvalcp.j ⊢ ∨ = ( join ‘ 𝐾 )
dihopelvalcp.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihopelvalcp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihopelvalcp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihopelvalcp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
dihopelvalcp.f ⊢ 𝐹 ∈ V
dihopelvalcp.s ⊢ 𝑆 ∈ V
Assertion dihopelvalc ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dihopelvalcp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihopelvalcp.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihopelvalcp.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dihopelvalcp.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 dihopelvalcp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 dihopelvalcp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 dihopelvalcp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
8 dihopelvalcp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
9 dihopelvalcp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
10 dihopelvalcp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11 dihopelvalcp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
12 dihopelvalcp.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
13 dihopelvalcp.f ⊢ 𝐹 ∈ V
14 dihopelvalcp.s ⊢ 𝑆 ∈ V
15 eqid ⊢ ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
16 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
18 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
19 eqid ⊢ ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
20 eqid ⊢ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
21 eqid ⊢ ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
22 eqid ⊢ ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( ℎ ∈ 𝑇 ↦ ( ( 𝑎 ‘ ℎ ) ∘ ( 𝑏 ‘ ℎ ) ) ) ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( ℎ ∈ 𝑇 ↦ ( ( 𝑎 ‘ ℎ ) ∘ ( 𝑏 ‘ ℎ ) ) ) )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 dihopelvalcpre ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )