Metamath Proof Explorer

Theorem diaffval

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

Ref Expression
Hypotheses diaval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
diaval.l ⊢ ≤ = ( le ‘ 𝐾 )
diaval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion diaffval ( 𝐾 ∈ 𝑉 → ( DIsoA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 diaval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 diaval.l ⊢ ≤ = ( le ‘ 𝐾 )
3 diaval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 elex ⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
5 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
6 5 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
7 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
9 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
10 9 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
11 10 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑦 ( le ‘ 𝑘 ) 𝑤 ↔ 𝑦 ≤ 𝑤 ) )
12 8 11 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } = { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } )
13 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
14 13 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
15 fveq2 ⊢ ( 𝑘 = 𝐾 → ( trL ‘ 𝑘 ) = ( trL ‘ 𝐾 ) )
16 15 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) )
17 16 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) )
18 eqidd ⊢ ( 𝑘 = 𝐾 → 𝑥 = 𝑥 )
19 17 10 18 breq123d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 ) )
20 14 19 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } )
21 12 20 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } ) )
22 6 21 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } ) ) )
23 df-disoa ⊢ DIsoA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑘 ) ∣ 𝑦 ( le ‘ 𝑘 ) 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ( le ‘ 𝑘 ) 𝑥 } ) ) )
24 22 23 3 mptfvmpt ⊢ ( 𝐾 ∈ V → ( DIsoA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } ) ) )
25 4 24 syl ⊢ ( 𝐾 ∈ 𝑉 → ( DIsoA ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ≤ 𝑥 } ) ) )