Metamath Proof Explorer


Theorem cdlemd5

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

Ref Expression
Hypotheses cdlemd4.l = ( le ‘ 𝐾 )
cdlemd4.j = ( join ‘ 𝐾 )
cdlemd4.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemd4.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemd4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemd5 ( ( ( ( 𝐾 ∈ 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 fveq2 ( 𝑅 = 𝑃 → ( 𝐹𝑅 ) = ( 𝐹𝑃 ) )
7 fveq2 ( 𝑅 = 𝑃 → ( 𝐺𝑅 ) = ( 𝐺𝑃 ) )
8 6 7 eqeq12d ( 𝑅 = 𝑃 → ( ( 𝐹𝑅 ) = ( 𝐺𝑅 ) ↔ ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ) )
9 simpll1 ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) )
10 simpl21 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
11 10 adantr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
12 simpl22 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
13 12 adantr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
14 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → 𝑃𝑄 )
15 14 ad2antrr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → 𝑃𝑄 )
16 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → 𝑅 ( 𝑃 𝑄 ) )
17 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → 𝑅𝑃 )
18 15 16 17 3jca ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) )
19 simpll3 ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) )
20 1 2 3 4 5 cdlemd4 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )
21 9 11 13 18 19 20 syl131anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑅𝑃 ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )
22 simpl3l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝐹𝑃 ) = ( 𝐺𝑃 ) )
23 8 21 22 pm2.61ne ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )
24 simpl1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) )
25 simpl21 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
26 simpl22 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
27 simpl23 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑃𝑄 )
28 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
29 27 28 jca ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) )
30 simpl3 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) )
31 1 2 3 4 5 cdlemd2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )
32 24 25 26 29 30 31 syl131anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )
33 23 32 pm2.61dan ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑅𝐴 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑃𝑄 ) ∧ ( ( 𝐹𝑃 ) = ( 𝐺𝑃 ) ∧ ( 𝐹𝑄 ) = ( 𝐺𝑄 ) ) ) → ( 𝐹𝑅 ) = ( 𝐺𝑅 ) )