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 ⊢ B = Base K
cdlemn4.l ⊢ ≤ ˙ = ≤ K
cdlemn4.a ⊢ A = Atoms ⁡ K
cdlemn4.p ⊢ P = oc ⁡ K ⁡ W
cdlemn4.h ⊢ H = LHyp ⁡ K
cdlemn4.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemn4.o ⊢ O = h ∈ T ⟼ I ↾ B
cdlemn4.u ⊢ U = DVecH ⁡ K ⁡ W
cdlemn4.f ⊢ F = ι h ∈ T | h ⁡ P = Q
cdlemn4.g ⊢ G = ι h ∈ T | h ⁡ P = R
cdlemn4.j ⊢ J = ι h ∈ T | h ⁡ Q = R
cdlemn4.s ⊢ + ˙ = + U
Assertion cdlemn4 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → G I ↾ T = F I ↾ T + ˙ J O

Proof

Step Hyp Ref Expression
1 cdlemn4.b ⊢ B = Base K
2 cdlemn4.l ⊢ ≤ ˙ = ≤ K
3 cdlemn4.a ⊢ A = Atoms ⁡ K
4 cdlemn4.p ⊢ P = oc ⁡ K ⁡ W
5 cdlemn4.h ⊢ H = LHyp ⁡ K
6 cdlemn4.t ⊢ T = LTrn ⁡ K ⁡ W
7 cdlemn4.o ⊢ O = h ∈ T ⟼ I ↾ B
8 cdlemn4.u ⊢ U = DVecH ⁡ K ⁡ W
9 cdlemn4.f ⊢ F = ι h ∈ T | h ⁡ P = Q
10 cdlemn4.g ⊢ G = ι h ∈ T | h ⁡ P = R
11 cdlemn4.j ⊢ J = ι h ∈ T | h ⁡ Q = R
12 cdlemn4.s ⊢ + ˙ = + U
13 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → K ∈ HL ∧ W ∈ H
14 2 3 5 4 lhpocnel2 ⊢ K ∈ HL ∧ W ∈ H → P ∈ A ∧ ¬ P ≤ ˙ W
15 13 14 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → P ∈ A ∧ ¬ P ≤ ˙ W
16 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → Q ∈ A ∧ ¬ Q ≤ ˙ W
17 2 3 5 6 9 ltrniotacl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ∈ T
18 13 15 16 17 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → F ∈ T
19 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
20 5 6 19 tendoidcl ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ TEndo ⁡ K ⁡ W
21 13 20 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → I ↾ T ∈ TEndo ⁡ K ⁡ W
22 2 3 5 6 11 ltrniotacl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → J ∈ T
23 1 5 6 19 7 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → O ∈ TEndo ⁡ K ⁡ W
24 13 23 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → O ∈ TEndo ⁡ K ⁡ W
25 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
26 eqid ⊢ + Scalar ⁡ U = + Scalar ⁡ U
27 5 6 19 8 25 12 26 dvhopvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ I ↾ T ∈ TEndo ⁡ K ⁡ W ∧ J ∈ T ∧ O ∈ TEndo ⁡ K ⁡ W → F I ↾ T + ˙ J O = F ∘ J I ↾ T + Scalar ⁡ U O
28 13 18 21 22 24 27 syl122anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → F I ↾ T + ˙ J O = F ∘ J I ↾ T + Scalar ⁡ U O
29 5 6 ltrncom ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ J ∈ T → F ∘ J = J ∘ F
30 13 18 22 29 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → F ∘ J = J ∘ F
31 2 3 4 5 6 9 10 11 cdlemn3 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → J ∘ F = G
32 30 31 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → F ∘ J = G
33 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
34 5 33 8 25 dvhsca ⊢ K ∈ HL ∧ W ∈ H → Scalar ⁡ U = EDRing ⁡ K ⁡ W
35 34 fveq2d ⊢ K ∈ HL ∧ W ∈ H → 0 Scalar ⁡ U = 0 EDRing ⁡ K ⁡ W
36 eqid ⊢ 0 EDRing ⁡ K ⁡ W = 0 EDRing ⁡ K ⁡ W
37 1 5 6 33 7 36 erng0g ⊢ K ∈ HL ∧ W ∈ H → 0 EDRing ⁡ K ⁡ W = O
38 35 37 eqtrd ⊢ K ∈ HL ∧ W ∈ H → 0 Scalar ⁡ U = O
39 13 38 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → 0 Scalar ⁡ U = O
40 39 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → I ↾ T + Scalar ⁡ U 0 Scalar ⁡ U = I ↾ T + Scalar ⁡ U O
41 5 33 erngdv ⊢ K ∈ HL ∧ W ∈ H → EDRing ⁡ K ⁡ W ∈ DivRing
42 drnggrp ⊢ EDRing ⁡ K ⁡ W ∈ DivRing → EDRing ⁡ K ⁡ W ∈ Grp
43 41 42 syl ⊢ K ∈ HL ∧ W ∈ H → EDRing ⁡ K ⁡ W ∈ Grp
44 34 43 eqeltrd ⊢ K ∈ HL ∧ W ∈ H → Scalar ⁡ U ∈ Grp
45 13 44 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → Scalar ⁡ U ∈ Grp
46 eqid ⊢ Base Scalar ⁡ U = Base Scalar ⁡ U
47 5 19 8 25 46 dvhbase ⊢ K ∈ HL ∧ W ∈ H → Base Scalar ⁡ U = TEndo ⁡ K ⁡ W
48 13 47 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → Base Scalar ⁡ U = TEndo ⁡ K ⁡ W
49 21 48 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → I ↾ T ∈ Base Scalar ⁡ U
50 eqid ⊢ 0 Scalar ⁡ U = 0 Scalar ⁡ U
51 46 26 50 grprid ⊢ Scalar ⁡ U ∈ Grp ∧ I ↾ T ∈ Base Scalar ⁡ U → I ↾ T + Scalar ⁡ U 0 Scalar ⁡ U = I ↾ T
52 45 49 51 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → I ↾ T + Scalar ⁡ U 0 Scalar ⁡ U = I ↾ T
53 40 52 eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → I ↾ T + Scalar ⁡ U O = I ↾ T
54 32 53 opeq12d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → F ∘ J I ↾ T + Scalar ⁡ U O = G I ↾ T
55 28 54 eqtr2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ R ∈ A ∧ ¬ R ≤ ˙ W → G I ↾ T = F I ↾ T + ˙ J O