Metamath Proof Explorer


Theorem cdlemn8

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 cdlemn8 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( 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 coass ( ( 𝐹𝐹 ) ∘ 𝑔 ) = ( 𝐹 ∘ ( 𝐹𝑔 ) )
14 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
15 2 3 4 5 lhpocnel2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
16 15 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
17 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
18 2 3 4 7 11 ltrniotacl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → 𝐹𝑇 )
19 14 16 17 18 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐹𝑇 )
20 1 4 7 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 : 𝐵1-1-onto𝐵 )
21 14 19 20 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐹 : 𝐵1-1-onto𝐵 )
22 f1ococnv1 ( 𝐹 : 𝐵1-1-onto𝐵 → ( 𝐹𝐹 ) = ( I ↾ 𝐵 ) )
23 21 22 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐹𝐹 ) = ( I ↾ 𝐵 ) )
24 23 coeq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( 𝐹𝐹 ) ∘ 𝑔 ) = ( ( I ↾ 𝐵 ) ∘ 𝑔 ) )
25 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝑔𝑇 )
26 1 4 7 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑔𝑇 ) → 𝑔 : 𝐵1-1-onto𝐵 )
27 14 25 26 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 : 𝐵1-1-onto𝐵 )
28 f1of ( 𝑔 : 𝐵1-1-onto𝐵𝑔 : 𝐵𝐵 )
29 fcoi2 ( 𝑔 : 𝐵𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝑔 ) = 𝑔 )
30 27 28 29 3syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( I ↾ 𝐵 ) ∘ 𝑔 ) = 𝑔 )
31 24 30 eqtr2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 = ( ( 𝐹𝐹 ) ∘ 𝑔 ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 cdlemn7 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐺 = ( ( 𝑠𝐹 ) ∘ 𝑔 ) ∧ ( I ↾ 𝑇 ) = 𝑠 ) )
33 32 simpld ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐺 = ( ( 𝑠𝐹 ) ∘ 𝑔 ) )
34 32 simprd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( I ↾ 𝑇 ) = 𝑠 )
35 34 fveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( I ↾ 𝑇 ) ‘ 𝐹 ) = ( 𝑠𝐹 ) )
36 fvresi ( 𝐹𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝐹 ) = 𝐹 )
37 19 36 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( I ↾ 𝑇 ) ‘ 𝐹 ) = 𝐹 )
38 35 37 eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑠𝐹 ) = 𝐹 )
39 38 coeq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( 𝑠𝐹 ) ∘ 𝑔 ) = ( 𝐹𝑔 ) )
40 33 39 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐺 = ( 𝐹𝑔 ) )
41 40 coeq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐹𝐺 ) = ( 𝐹 ∘ ( 𝐹𝑔 ) ) )
42 13 31 41 3eqtr4a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 = ( 𝐹𝐺 ) )
43 4 7 ltrncnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹𝑇 )
44 14 19 43 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐹𝑇 )
45 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
46 2 3 4 7 12 ltrniotacl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) → 𝐺𝑇 )
47 14 16 45 46 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝐺𝑇 )
48 4 7 ltrncom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) → ( 𝐹𝐺 ) = ( 𝐺 𝐹 ) )
49 14 44 47 48 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐹𝐺 ) = ( 𝐺 𝐹 ) )
50 42 49 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑠𝐸𝑔𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠𝐹 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 = ( 𝐺 𝐹 ) )