Metamath Proof Explorer

Theorem cdlemg44

Description: Part of proof of Lemma G of Crawley p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg44.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg44.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg44.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg44 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 cdlemg44.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 cdlemg44.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 cdlemg44.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 4 5 1 lhpexnle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
7 6 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
8 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → 𝐹 ∈ 𝑇 )
10 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → 𝐺 ∈ 𝑇 )
11 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
12 8 9 10 11 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
13 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 )
14 8 10 9 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 )
15 3simpc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
16 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
17 1 2 3 4 5 cdlemg44b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑝 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑝 ) ) )
18 8 9 10 15 16 17 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑝 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑝 ) ) )
19 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) )
20 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
21 4 5 1 2 ltrncoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑝 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑝 ) ) )
22 8 19 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑝 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑝 ) ) )
23 4 5 1 2 ltrncoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑝 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑝 ) ) )
24 8 10 9 20 23 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑝 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑝 ) ) )
25 18 22 24 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑝 ) = ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑝 ) )
26 4 5 1 2 cdlemd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ∧ ( 𝐺 ∘ 𝐹 ) ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑝 ) = ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑝 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )
27 8 12 14 15 25 26 syl311anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )
28 27 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) ) )
29 7 28 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐺 ∘ 𝐹 ) )