Metamath Proof Explorer

Theorem dibffval

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

Ref Expression
Hypotheses dibval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dibval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion dibffval ( 𝐾 ∈ 𝑉 → ( DIsoB ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 dibval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dibval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 elex ⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
4 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
5 4 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( DIsoA ‘ 𝑘 ) = ( DIsoA ‘ 𝐾 ) )
7 6 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) )
8 7 dmeqd ⊢ ( 𝑘 = 𝐾 → dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) = dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) )
9 7 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) = ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) )
10 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
11 10 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
12 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
13 12 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
14 13 reseq2d ⊢ ( 𝑘 = 𝐾 → ( I ↾ ( Base ‘ 𝑘 ) ) = ( I ↾ 𝐵 ) )
15 11 14 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) )
16 15 sneqd ⊢ ( 𝑘 = 𝐾 → { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } = { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } )
17 9 16 xpeq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) )
18 8 17 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) = ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) ) )
19 5 18 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) ) ) )
20 df-dib ⊢ DIsoB = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) ) )
21 19 20 2 mptfvmpt ⊢ ( 𝐾 ∈ V → ( DIsoB ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) ) ) )
22 3 21 syl ⊢ ( 𝐾 ∈ 𝑉 → ( DIsoB ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( I ↾ 𝐵 ) ) } ) ) ) )