Theorem dibopelvalN

Description: Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dibval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dibval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dibval.o	⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dibval.j	⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dibval.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dibopelvalN	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dibval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dibval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dibval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dibval.o	⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
5		dibval.j	⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6		dibval.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
7	1 2 3 4 5 6	dibval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( 𝐼 ‘ 𝑋 ) = ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) )
8	7	eleq2d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) ) )
9		opelxp	⊢ ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) ↔ ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 ∈ { 0 } ) )
10	3	fvexi	⊢ 𝑇 ∈ V
11	10	mptex	⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ∈ V
12	4 11	eqeltri	⊢ 0 ∈ V
13	12	elsn2	⊢ ( 𝑆 ∈ { 0 } ↔ 𝑆 = 0 )
14	13	anbi2i	⊢ ( ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 ∈ { 0 } ) ↔ ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 = 0 ) )
15	9 14	bitri	⊢ ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) ↔ ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 = 0 ) )
16	8 15	bitrdi	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( 𝐽 ‘ 𝑋 ) ∧ 𝑆 = 0 ) ) )