Metamath Proof Explorer

Theorem cdleml1N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleml1.b ⊢ B = Base K
cdleml1.h ⊢ H = LHyp ⁡ K
cdleml1.t ⊢ T = LTrn ⁡ K ⁡ W
cdleml1.r ⊢ R = trL ⁡ K ⁡ W
cdleml1.e ⊢ E = TEndo ⁡ K ⁡ W
Assertion cdleml1N ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f = R ⁡ V ⁡ f

Proof

Step Hyp Ref Expression
1 cdleml1.b ⊢ B = Base K
2 cdleml1.h ⊢ H = LHyp ⁡ K
3 cdleml1.t ⊢ T = LTrn ⁡ K ⁡ W
4 cdleml1.r ⊢ R = trL ⁡ K ⁡ W
5 cdleml1.e ⊢ E = TEndo ⁡ K ⁡ W
6 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → K ∈ HL ∧ W ∈ H
7 simp21 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → U ∈ E
8 simp23 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → f ∈ T
9 eqid ⊢ ≤ K = ≤ K
10 9 2 3 4 5 tendotp ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ f ∈ T → R ⁡ U ⁡ f ≤ K R ⁡ f
11 6 7 8 10 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f ≤ K R ⁡ f
12 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → K ∈ HL
13 hlatl ⊢ K ∈ HL → K ∈ AtLat
14 12 13 syl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → K ∈ AtLat
15 2 3 5 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ f ∈ T → U ⁡ f ∈ T
16 6 7 8 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → U ⁡ f ∈ T
17 simp32 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → U ⁡ f ≠ I ↾ B
18 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
19 1 18 2 3 4 trlnidat ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ f ∈ T ∧ U ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f ∈ Atoms ⁡ K
20 6 16 17 19 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f ∈ Atoms ⁡ K
21 simp31 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → f ≠ I ↾ B
22 1 18 2 3 4 trlnidat ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ f ≠ I ↾ B → R ⁡ f ∈ Atoms ⁡ K
23 6 8 21 22 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ f ∈ Atoms ⁡ K
24 9 18 atcmp ⊢ K ∈ AtLat ∧ R ⁡ U ⁡ f ∈ Atoms ⁡ K ∧ R ⁡ f ∈ Atoms ⁡ K → R ⁡ U ⁡ f ≤ K R ⁡ f ↔ R ⁡ U ⁡ f = R ⁡ f
25 14 20 23 24 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f ≤ K R ⁡ f ↔ R ⁡ U ⁡ f = R ⁡ f
26 11 25 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f = R ⁡ f
27 simp22 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → V ∈ E
28 9 2 3 4 5 tendotp ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ f ∈ T → R ⁡ V ⁡ f ≤ K R ⁡ f
29 6 27 8 28 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ V ⁡ f ≤ K R ⁡ f
30 2 3 5 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ f ∈ T → V ⁡ f ∈ T
31 6 27 8 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → V ⁡ f ∈ T
32 simp33 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → V ⁡ f ≠ I ↾ B
33 1 18 2 3 4 trlnidat ⊢ K ∈ HL ∧ W ∈ H ∧ V ⁡ f ∈ T ∧ V ⁡ f ≠ I ↾ B → R ⁡ V ⁡ f ∈ Atoms ⁡ K
34 6 31 32 33 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ V ⁡ f ∈ Atoms ⁡ K
35 9 18 atcmp ⊢ K ∈ AtLat ∧ R ⁡ V ⁡ f ∈ Atoms ⁡ K ∧ R ⁡ f ∈ Atoms ⁡ K → R ⁡ V ⁡ f ≤ K R ⁡ f ↔ R ⁡ V ⁡ f = R ⁡ f
36 14 34 23 35 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ V ⁡ f ≤ K R ⁡ f ↔ R ⁡ V ⁡ f = R ⁡ f
37 29 36 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ V ⁡ f = R ⁡ f
38 26 37 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → R ⁡ U ⁡ f = R ⁡ V ⁡ f