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 ‘ 𝐾 ) ‘ 𝑤 ) ) } ) ) )