Theorem cdlemn7

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 26-Feb-2014)

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

Proof

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