Theorem dihordlem7

Description: Part of proof of Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dihordlem8.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihordlem8.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihordlem8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihordlem8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihordlem8.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	dihordlem8.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dihordlem8.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dihordlem8.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dihordlem8.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihordlem8.s	⊢ + = ( +g ‘ 𝑈 )
	dihordlem8.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
Assertion	dihordlem7	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑓 = ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) ∧ 𝑂 = 𝑠 ) )

Proof

Step	Hyp	Ref	Expression
1		dihordlem8.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihordlem8.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dihordlem8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		dihordlem8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		dihordlem8.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
6		dihordlem8.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7		dihordlem8.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8		dihordlem8.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
9		dihordlem8.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
10		dihordlem8.s	⊢ + = ( +g ‘ 𝑈 )
11		dihordlem8.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
12		simp33	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) )
13		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
15		simp2r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
16		simp31	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → 𝑠 ∈ 𝐸 )
17		simp32	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 ∈ 𝑇 )
18	1 2 3 4 5 6 7 8 9 10 11	dihordlem6	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ) → ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) = ⟨ ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) , 𝑠 ⟩ )
19	13 14 15 16 17 18	syl122anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) = ⟨ ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) , 𝑠 ⟩ )
20	12 19	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ⟨ 𝑓 , 𝑂 ⟩ = ⟨ ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) , 𝑠 ⟩ )
21		fvex	⊢ ( 𝑠 ‘ 𝐺 ) ∈ V
22		vex	⊢ 𝑔 ∈ V
23	21 22	coex	⊢ ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) ∈ V
24		vex	⊢ 𝑠 ∈ V
25	23 24	opth2	⊢ ( ⟨ 𝑓 , 𝑂 ⟩ = ⟨ ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) , 𝑠 ⟩ ↔ ( 𝑓 = ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) ∧ 𝑂 = 𝑠 ) )
26	20 25	sylib	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠 ‘ 𝐺 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑓 = ( ( 𝑠 ‘ 𝐺 ) ∘ 𝑔 ) ∧ 𝑂 = 𝑠 ) )