Metamath Proof Explorer

Theorem cdleml2N

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 cdleml2N ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → ∃ s ∈ E s ⁡ U ⁡ f = 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 2 3 5 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ f ∈ T → U ⁡ f ∈ T
10 6 7 8 9 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
11 simp22 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → V ∈ E
12 2 3 5 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ f ∈ T → V ⁡ f ∈ T
13 6 11 8 12 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
14 1 2 3 4 5 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
15 2 3 4 5 cdlemk ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ f ∈ T ∧ V ⁡ f ∈ T ∧ R ⁡ U ⁡ f = R ⁡ V ⁡ f → ∃ s ∈ E s ⁡ U ⁡ f = V ⁡ f
16 6 10 13 14 15 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ f ∈ T ∧ f ≠ I ↾ B ∧ U ⁡ f ≠ I ↾ B ∧ V ⁡ f ≠ I ↾ B → ∃ s ∈ E s ⁡ U ⁡ f = V ⁡ f