Metamath Proof Explorer


Theorem cdlemk38

Description: Part of proof of Lemma K of Crawley p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 ? (Contributed by NM, 19-Jul-2013)

Ref Expression
Hypotheses cdlemk4.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk4.l = ( le ‘ 𝐾 )
cdlemk4.j = ( join ‘ 𝐾 )
cdlemk4.m = ( meet ‘ 𝐾 )
cdlemk4.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk4.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk4.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk4.z 𝑍 = ( ( 𝑃 ( 𝑅𝑏 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑏 𝐹 ) ) ) )
cdlemk4.y 𝑌 = ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑍 ( 𝑅 ‘ ( 𝐺 𝑏 ) ) ) )
cdlemk4.x 𝑋 = ( 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑧𝑃 ) = 𝑌 ) )
Assertion cdlemk38 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk4.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk4.l = ( le ‘ 𝐾 )
3 cdlemk4.j = ( join ‘ 𝐾 )
4 cdlemk4.m = ( meet ‘ 𝐾 )
5 cdlemk4.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk4.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk4.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk4.z 𝑍 = ( ( 𝑃 ( 𝑅𝑏 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑏 𝐹 ) ) ) )
10 cdlemk4.y 𝑌 = ( ( 𝑃 ( 𝑅𝐺 ) ) ( 𝑍 ( 𝑅 ‘ ( 𝐺 𝑏 ) ) ) )
11 cdlemk4.x 𝑋 = ( 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑧𝑃 ) = 𝑌 ) )
12 1 6 7 8 cdlemftr2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑏𝑇 ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) )
13 12 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ∃ 𝑏𝑇 ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) )
14 nfv 𝑏 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
15 nfra1 𝑏𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑧𝑃 ) = 𝑌 )
16 nfcv 𝑏 𝑇
17 15 16 nfriota 𝑏 ( 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑧𝑃 ) = 𝑌 ) )
18 11 17 nfcxfr 𝑏 𝑋
19 nfcv 𝑏 𝑃
20 18 19 nffv 𝑏 ( 𝑋𝑃 )
21 nfcv 𝑏
22 nfcv 𝑏 ( 𝑃 ( 𝑅𝐺 ) )
23 20 21 22 nfbr 𝑏 ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) )
24 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
25 simpl21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) )
26 simpl22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) )
27 simpl23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑁𝑇 )
28 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
29 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
30 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) )
31 1 2 3 4 5 6 7 8 9 10 11 cdlemk37 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )
32 24 25 26 27 28 29 30 31 syl331anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )
33 32 exp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝑏𝑇 → ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) ) ) )
34 14 23 33 rexlimd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( ∃ 𝑏𝑇 ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) ) )
35 13 34 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝑋𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )