Theorem dibval

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

	Ref	Expression
Hypotheses	dibval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dibval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dibval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dibval.o	⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dibval.j	⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dibval.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dibval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 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	dibfval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) )
8	7	adantr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → 𝐼 = ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) )
9	8	fveq1d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( 𝐼 ‘ 𝑋 ) = ( ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) ‘ 𝑋 ) )
10		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐽 ‘ 𝑥 ) = ( 𝐽 ‘ 𝑋 ) )
11	10	xpeq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) = ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) )
12		eqid	⊢ ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) = ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) )
13		fvex	⊢ ( 𝐽 ‘ 𝑋 ) ∈ V
14		snex	⊢ { 0 } ∈ V
15	13 14	xpex	⊢ ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) ∈ V
16	11 12 15	fvmpt	⊢ ( 𝑋 ∈ dom 𝐽 → ( ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) ‘ 𝑋 ) = ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) )
17	16	adantl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( ( 𝑥 ∈ dom 𝐽 ↦ ( ( 𝐽 ‘ 𝑥 ) × { 0 } ) ) ‘ 𝑋 ) = ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) )
18	9 17	eqtrd	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐽 ) → ( 𝐼 ‘ 𝑋 ) = ( ( 𝐽 ‘ 𝑋 ) × { 0 } ) )