# 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 ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑃 ) = 𝑃 ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )