Metamath Proof Explorer

Theorem cdlemj2

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate p . (Contributed by NM, 20-Jun-2013)

Ref Expression
Hypotheses cdlemj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemj.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemj2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )

Proof

Step Hyp Ref Expression
1 cdlemj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 cdlemj.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 cdlemj.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemj.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 simpl1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) )
7 simpl2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) )
8 simpl3l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) )
9 simpl3r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) )
10 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
13 1 2 3 4 5 11 12 cdlemj1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) )
14 6 7 8 9 10 13 syl113anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) )
15 14 exp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) ) ) )
16 15 ralrimiv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) ) )
17 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → 𝑈 ∈ 𝐸 )
19 simp133 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ℎ ∈ 𝑇 )
20 2 3 5 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ ℎ ∈ 𝑇 ) → ( 𝑈 ‘ ℎ ) ∈ 𝑇 )
21 17 18 19 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑈 ‘ ℎ ) ∈ 𝑇 )
22 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → 𝑉 ∈ 𝐸 )
23 2 3 5 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ ℎ ∈ 𝑇 ) → ( 𝑉 ‘ ℎ ) ∈ 𝑇 )
24 17 22 19 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑉 ‘ ℎ ) ∈ 𝑇 )
25 11 12 2 3 ltrneq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ ℎ ) ∈ 𝑇 ∧ ( 𝑉 ‘ ℎ ) ∈ 𝑇 ) → ( ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) ) ↔ ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) ) )
26 17 21 24 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) ) ↔ ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) ) )
27 16 26 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )