Metamath Proof Explorer

Theorem erngdvlem4

Description: Lemma for erngdv . (Contributed by NM, 11-Aug-2013)

Ref Expression
Hypotheses ernggrp.h ⊢ H = LHyp ⁡ K
ernggrp.d ⊢ D = EDRing ⁡ K ⁡ W
erngdv.b ⊢ B = Base K
erngdv.t ⊢ T = LTrn ⁡ K ⁡ W
erngdv.e ⊢ E = TEndo ⁡ K ⁡ W
erngdv.p ⊢ P = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
erngdv.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
erngdv.i ⊢ I = a ∈ E ⟼ f ∈ T ⟼ a ⁡ f -1
erngrnglem.m ⊢ + ˙ = a ∈ E , b ∈ E ⟼ a ∘ b
edlemk6.j ⊢ ∨ ˙ = join ⁡ K
edlemk6.m ⊢ ∧ ˙ = meet ⁡ K
edlemk6.r ⊢ R = trL ⁡ K ⁡ W
edlemk6.p ⊢ Q = oc ⁡ K ⁡ W
edlemk6.z ⊢ Z = Q ∨ ˙ R ⁡ b ∧ ˙ h ⁡ Q ∨ ˙ R ⁡ b ∘ s ⁡ h -1
edlemk6.y ⊢ Y = Q ∨ ˙ R ⁡ g ∧ ˙ Z ∨ ˙ R ⁡ g ∘ b -1
edlemk6.x ⊢ X = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ s ⁡ h ∧ R ⁡ b ≠ R ⁡ g → z ⁡ Q = Y
edlemk6.u ⊢ U = g ∈ T ⟼ if s ⁡ h = h g X
Assertion erngdvlem4 ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → D ∈ DivRing

Proof

Step Hyp Ref Expression
1 ernggrp.h ⊢ H = LHyp ⁡ K
2 ernggrp.d ⊢ D = EDRing ⁡ K ⁡ W
3 erngdv.b ⊢ B = Base K
4 erngdv.t ⊢ T = LTrn ⁡ K ⁡ W
5 erngdv.e ⊢ E = TEndo ⁡ K ⁡ W
6 erngdv.p ⊢ P = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
7 erngdv.o ⊢ 0 ˙ = f ∈ T ⟼ I ↾ B
8 erngdv.i ⊢ I = a ∈ E ⟼ f ∈ T ⟼ a ⁡ f -1
9 erngrnglem.m ⊢ + ˙ = a ∈ E , b ∈ E ⟼ a ∘ b
10 edlemk6.j ⊢ ∨ ˙ = join ⁡ K
11 edlemk6.m ⊢ ∧ ˙ = meet ⁡ K
12 edlemk6.r ⊢ R = trL ⁡ K ⁡ W
13 edlemk6.p ⊢ Q = oc ⁡ K ⁡ W
14 edlemk6.z ⊢ Z = Q ∨ ˙ R ⁡ b ∧ ˙ h ⁡ Q ∨ ˙ R ⁡ b ∘ s ⁡ h -1
15 edlemk6.y ⊢ Y = Q ∨ ˙ R ⁡ g ∧ ˙ Z ∨ ˙ R ⁡ g ∘ b -1
16 edlemk6.x ⊢ X = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ s ⁡ h ∧ R ⁡ b ≠ R ⁡ g → z ⁡ Q = Y
17 edlemk6.u ⊢ U = g ∈ T ⟼ if s ⁡ h = h g X
18 eqid ⊢ Base D = Base D
19 1 4 5 2 18 erngbase ⊢ K ∈ HL ∧ W ∈ H → Base D = E
20 19 eqcomd ⊢ K ∈ HL ∧ W ∈ H → E = Base D
21 20 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → E = Base D
22 eqid ⊢ ⋅ D = ⋅ D
23 1 4 5 2 22 erngfmul ⊢ K ∈ HL ∧ W ∈ H → ⋅ D = a ∈ E , b ∈ E ⟼ a ∘ b
24 9 23 eqtr4id ⊢ K ∈ HL ∧ W ∈ H → + ˙ = ⋅ D
25 24 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → + ˙ = ⋅ D
26 3 1 4 5 7 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ E
27 26 19 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base D
28 eqid ⊢ + D = + D
29 1 4 5 2 28 erngfplus ⊢ K ∈ HL ∧ W ∈ H → + D = a ∈ E , b ∈ E ⟼ f ∈ T ⟼ a ⁡ f ∘ b ⁡ f
30 6 29 eqtr4id ⊢ K ∈ HL ∧ W ∈ H → P = + D
31 30 oveqd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ P 0 ˙ = 0 ˙ + D 0 ˙
32 3 1 4 5 7 6 tendo0pl ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ E → 0 ˙ P 0 ˙ = 0 ˙
33 26 32 mpdan ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ P 0 ˙ = 0 ˙
34 31 33 eqtr3d ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ + D 0 ˙ = 0 ˙
35 1 2 3 4 5 6 7 8 erngdvlem1 ⊢ K ∈ HL ∧ W ∈ H → D ∈ Grp
36 eqid ⊢ 0 D = 0 D
37 18 28 36 isgrpid2 ⊢ D ∈ Grp → 0 ˙ ∈ Base D ∧ 0 ˙ + D 0 ˙ = 0 ˙ ↔ 0 D = 0 ˙
38 35 37 syl ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base D ∧ 0 ˙ + D 0 ˙ = 0 ˙ ↔ 0 D = 0 ˙
39 27 34 38 mpbi2and ⊢ K ∈ HL ∧ W ∈ H → 0 D = 0 ˙
40 39 eqcomd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ = 0 D
41 40 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → 0 ˙ = 0 D
42 1 2 3 4 5 6 7 8 9 erngdvlem3 ⊢ K ∈ HL ∧ W ∈ H → D ∈ Ring
43 1 4 5 2 42 erng1lem ⊢ K ∈ HL ∧ W ∈ H → 1 D = I ↾ T
44 43 eqcomd ⊢ K ∈ HL ∧ W ∈ H → I ↾ T = 1 D
45 44 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → I ↾ T = 1 D
46 42 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → D ∈ Ring
47 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → K ∈ HL ∧ W ∈ H
48 24 oveqd ⊢ K ∈ HL ∧ W ∈ H → s + ˙ t = s ⋅ D t
49 47 48 syl ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s + ˙ t = s ⋅ D t
50 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s ∈ E
51 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → t ∈ E
52 1 4 5 2 22 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ t ∈ E → s ⋅ D t = s ∘ t
53 47 50 51 52 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s ⋅ D t = s ∘ t
54 49 53 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s + ˙ t = s ∘ t
55 3 1 4 5 7 tendoconid ⊢ K ∈ HL ∧ W ∈ H ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s ∘ t ≠ 0 ˙
56 55 3adant1r ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s ∘ t ≠ 0 ˙
57 54 56 eqnetrd ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ ∧ t ∈ E ∧ t ≠ 0 ˙ → s + ˙ t ≠ 0 ˙
58 3 1 4 5 7 tendo1ne0 ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ≠ 0 ˙
59 58 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → I ↾ T ≠ 0 ˙
60 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → K ∈ HL ∧ W ∈ H
61 simplrl ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → h ∈ T
62 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → s ∈ E ∧ s ≠ 0 ˙
63 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml6 ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ s ∈ E ∧ s ≠ 0 ˙ → U ∈ E ∧ U ⁡ s ⁡ h = h
64 63 simpld ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ s ∈ E ∧ s ≠ 0 ˙ → U ∈ E
65 60 61 62 64 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ∈ E
66 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml9 ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ≠ 0 ˙
67 66 3expa ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ≠ 0 ˙
68 24 oveqd ⊢ K ∈ HL ∧ W ∈ H → U + ˙ s = U ⋅ D s
69 68 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U + ˙ s = U ⋅ D s
70 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → s ∈ E
71 1 4 5 2 22 erngmul ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ s ∈ E → U ⋅ D s = U ∘ s
72 60 65 70 71 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ⋅ D s = U ∘ s
73 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml8 ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ∘ s = I ↾ T
74 73 3expa ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U ∘ s = I ↾ T
75 69 72 74 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B ∧ s ∈ E ∧ s ≠ 0 ˙ → U + ˙ s = I ↾ T
76 21 25 41 45 46 57 59 65 67 75 isdrngd ⊢ K ∈ HL ∧ W ∈ H ∧ h ∈ T ∧ h ≠ I ↾ B → D ∈ DivRing