This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dicffval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013)

Ref Expression
Hypotheses dicval.l ⊢ ≤ = ( le ‘ 𝐾 )
dicval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dicval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion dicffval ( 𝐾 ∈ 𝑉 → ( DIsoC ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 dicval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dicval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 dicval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 elex ⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
5 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
6 5 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
7 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
8 7 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
9 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
10 9 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
11 10 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑟 ( le ‘ 𝑘 ) 𝑤 ↔ 𝑟 ≤ 𝑤 ) )
12 11 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 ↔ ¬ 𝑟 ≤ 𝑤 ) )
13 8 12 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑟 ∈ ( Atoms ‘ 𝑘 ) ∣ ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 } = { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } )
14 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
15 14 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
16 fveq2 ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ( oc ‘ 𝐾 ) )
17 16 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) )
18 17 fveqeq2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ↔ ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) )
19 15 18 riotaeqbidv ⊢ ( 𝑘 = 𝐾 → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) = ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) )
20 19 fveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) )
21 20 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ↔ 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ) )
22 fveq2 ⊢ ( 𝑘 = 𝐾 → ( TEndo ‘ 𝑘 ) = ( TEndo ‘ 𝐾 ) )
23 22 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) )
24 23 eleq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↔ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) )
25 21 24 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) ↔ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) ) )
26 25 opabbidv ⊢ ( 𝑘 = 𝐾 → { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) } = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } )
27 13 26 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑞 ∈ { 𝑟 ∈ ( Atoms ‘ 𝑘 ) ∣ ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) } ) = ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } ) )
28 6 27 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑞 ∈ { 𝑟 ∈ ( Atoms ‘ 𝑘 ) ∣ ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ) )
29 df-dic ⊢ DIsoC = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑞 ∈ { 𝑟 ∈ ( Atoms ‘ 𝑘 ) ∣ ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ) )
30 28 29 3 mptfvmpt ⊢ ( 𝐾 ∈ V → ( DIsoC ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ) )
31 4 30 syl ⊢ ( 𝐾 ∈ 𝑉 → ( DIsoC ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ) )