Theorem dih1dimc

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

	Ref	Expression
Hypotheses	dih1dimc.l	⊢ ≤ = ( le ‘ 𝐾 )
	dih1dimc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dih1dimc.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih1dimc.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimc.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimc.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimc.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimc.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dih1dimc.f	⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
Assertion	dih1dimc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		dih1dimc.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dih1dimc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dih1dimc.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dih1dimc.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		dih1dimc.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dih1dimc.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7		dih1dimc.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8		dih1dimc.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
9		dih1dimc.f	⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
10		eqid	⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
11	1 2 3 10 6	dihvalcqat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) )
12	1 2 3 4 5 10 7 8 9	diclspsn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) )
13	11 12	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) )