Theorem dih1dimb2

Description: Isomorphism H at an atom under W . (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimb2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dih1dimb2.l	⊢ ≤ = ( le ‘ 𝐾 )
	dih1dimb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dih1dimb2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih1dimb2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb2.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dih1dimb2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
Assertion	dih1dimb2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dih1dimb2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dih1dimb2.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dih1dimb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		dih1dimb2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dih1dimb2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dih1dimb2.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7		dih1dimb2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8		dih1dimb2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9		dih1dimb2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
10		eqid	⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11	2 3 4 5 10	cdlemf	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 )
12		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 )
13		simp1rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑄 ∈ 𝐴 )
14	12 13	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 )
15		simp1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓 ∈ 𝑇 )
17	1 3 4 5 10	trlnidatb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) )
18	15 16 17	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) )
19	14 18	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓 ≠ ( I ↾ 𝐵 ) )
20	12	fveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝐼 ‘ 𝑄 ) )
21	1 4 5 10 6 7 8 9	dih1dimb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
22	15 16 21	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
23	20 22	eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) )
24	19 23	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )
25	24	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) ) )
26	25	reximdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) ) )
27	11 26	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑓 , 𝑂 ⟩ } ) ) )