Metamath Proof Explorer

Theorem cdlemn4

Description: Part of proof of Lemma N of Crawley p. 121 line 31. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses cdlemn4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemn4.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemn4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemn4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemn4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
cdlemn4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
cdlemn4.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
cdlemn4.j ⊢ 𝐽 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑄 ) = 𝑅 )
cdlemn4.s ⊢ + = ( +g ‘ 𝑈 )
Assertion cdlemn4 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ + ⟨ 𝐽 , 𝑂 ⟩ ) )

Proof

Step Hyp Ref Expression
1 cdlemn4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemn4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemn4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemn4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemn4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemn4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemn4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8 cdlemn4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemn4.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
10 cdlemn4.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
11 cdlemn4.j ⊢ 𝐽 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑄 ) = 𝑅 )
12 cdlemn4.s ⊢ + = ( +g ‘ 𝑈 )
13 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 2 3 5 4 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
15 13 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
16 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
17 2 3 5 6 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
18 13 15 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
19 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
20 5 6 19 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
21 13 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
22 2 3 5 6 11 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐽 ∈ 𝑇 )
23 1 5 6 19 7 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
24 13 23 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
25 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
26 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
27 5 6 19 8 25 12 26 dvhopvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝐽 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ + ⟨ 𝐽 , 𝑂 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐽 ) , ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
28 13 18 21 22 24 27 syl122anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ + ⟨ 𝐽 , 𝑂 ⟩ ) = ⟨ ( 𝐹 ∘ 𝐽 ) , ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
29 5 6 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐽 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐽 ) = ( 𝐽 ∘ 𝐹 ) )
30 13 18 22 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐹 ∘ 𝐽 ) = ( 𝐽 ∘ 𝐹 ) )
31 2 3 4 5 6 9 10 11 cdlemn3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐽 ∘ 𝐹 ) = 𝐺 )
32 30 31 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐹 ∘ 𝐽 ) = 𝐺 )
33 eqid ⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
34 5 33 8 25 dvhsca ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Scalar ‘ 𝑈 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
35 34 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
36 eqid ⊢ ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
37 1 5 6 33 7 36 erng0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑂 )
38 35 37 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = 𝑂 )
39 13 38 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = 𝑂 )
40 39 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) = ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) )
41 5 33 erngdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
42 drnggrp ⊢ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp )
43 41 42 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ Grp )
44 34 43 eqeltrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Scalar ‘ 𝑈 ) ∈ Grp )
45 13 44 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( Scalar ‘ 𝑈 ) ∈ Grp )
46 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
47 5 19 8 25 46 dvhbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
48 13 47 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
49 21 48 eleqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
50 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
51 46 26 50 grprid ⊢ ( ( ( Scalar ‘ 𝑈 ) ∈ Grp ∧ ( I ↾ 𝑇 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) = ( I ↾ 𝑇 ) )
52 45 49 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) = ( I ↾ 𝑇 ) )
53 40 52 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) = ( I ↾ 𝑇 ) )
54 32 53 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ ( 𝐹 ∘ 𝐽 ) , ( ( I ↾ 𝑇 ) ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ = ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ )
55 28 54 eqtr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ + ⟨ 𝐽 , 𝑂 ⟩ ) )