Metamath Proof Explorer

Theorem cdlemd8

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses cdlemd4.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemd4.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemd4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemd4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemd4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemd8 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑅 ) = ( 𝐺 ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cdlemd4.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemd4.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemd4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemd4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 cdlemd4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑃 )
7 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐹 ∈ 𝑇 )
9 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 1 3 4 5 ltrnideq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) )
12 7 8 9 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) )
13 6 12 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) )
14 13 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑅 ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ‘ 𝑅 ) )
15 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) )
16 15 6 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐺 ‘ 𝑃 ) = 𝑃 )
17 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐺 ∈ 𝑇 )
18 10 1 3 4 5 ltrnideq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) )
19 7 17 9 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) )
20 16 19 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) )
21 20 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐺 ‘ 𝑅 ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ‘ 𝑅 ) )
22 14 21 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑅 ) = ( 𝐺 ‘ 𝑅 ) )