Theorem dian0

Description: The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	dian0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dian0.l	⊢ ≤ = ( le ‘ 𝐾 )
	dian0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dian0.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dian0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		dian0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dian0.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dian0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dian0.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6	1 3 5	idltrn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
7	6	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
8		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9		eqid	⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
10	1 8 3 9	trlid0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
11	10	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) )
12		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
13	12	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ AtLat )
14		simpl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) → 𝑋 ∈ 𝐵 )
15	1 2 8	atl0le	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 0. ‘ 𝐾 ) ≤ 𝑋 )
16	13 14 15	syl2an	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 0. ‘ 𝐾 ) ≤ 𝑋 )
17	11 16	eqbrtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) ≤ 𝑋 )
18	1 2 3 5 9 4	diaelval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( I ↾ 𝐵 ) ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) ≤ 𝑋 ) ) )
19	7 17 18	mpbir2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( I ↾ 𝐵 ) ∈ ( 𝐼 ‘ 𝑋 ) )
20	19	ne0d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ≠ ∅ )