Metamath Proof Explorer

Theorem dicelval1sta

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 16-Feb-2014)

		Ref	Expression
	Hypotheses	dicelval1sta.l	⊢ ≤ = ( le ‘ 𝐾 )
		dicelval1sta.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
		dicelval1sta.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
		dicelval1sta.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
		dicelval1sta.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
		dicelval1sta.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
	Assertion	dicelval1sta	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dicelval1sta.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dicelval1sta.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dicelval1sta.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dicelval1sta.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		dicelval1sta.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dicelval1sta.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
7		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
8	1 2 3 4 5 7 6	dicval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
9	8	eleq2d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ↔ 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
10	9	biimp3a	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
11		eqeq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑌 ) → ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ↔ ( 1^st ‘ 𝑌 ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ) )
12	11	anbi1d	⊢ ( 𝑓 = ( 1^st ‘ 𝑌 ) → ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 1^st ‘ 𝑌 ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
13		fveq1	⊢ ( 𝑠 = ( 2^nd ‘ 𝑌 ) → ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )
14	13	eqeq2d	⊢ ( 𝑠 = ( 2^nd ‘ 𝑌 ) → ( ( 1^st ‘ 𝑌 ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ↔ ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ) )
15		eleq1	⊢ ( 𝑠 = ( 2^nd ‘ 𝑌 ) → ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
16	14 15	anbi12d	⊢ ( 𝑠 = ( 2^nd ‘ 𝑌 ) → ( ( ( 1^st ‘ 𝑌 ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
17	12 16	elopabi	⊢ ( 𝑌 ∈ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } → ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
18	10 17	syl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
19	18	simpld	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )