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 ↾ 𝑇 ) ⟩ +𝐽 , 𝑂 ⟩ ) )