This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erngdvlem4

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

Ref Expression
Hypotheses ernggrp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ernggrp.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
erngdv.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
erngdv.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngdv.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngdv.p ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
erngdv.o ⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
erngdv.i ⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑓 ) ) )
erngrnglem.m ⊢ + = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑎 ∘ 𝑏 ) )
edlemk6.j ⊢ ∨ = ( join ‘ 𝐾 )
edlemk6.m ⊢ ∧ = ( meet ‘ 𝐾 )
edlemk6.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
edlemk6.p ⊢ 𝑄 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
edlemk6.z ⊢ 𝑍 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑏 ) ) ∧ ( ( ℎ ‘ 𝑄 ) ∨ ( 𝑅 ‘ ( 𝑏 ∘ ◡ ( 𝑠 ‘ ℎ ) ) ) ) )
edlemk6.y ⊢ 𝑌 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) )
edlemk6.x ⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ ( 𝑠 ‘ ℎ ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑔 ) ) → ( 𝑧 ‘ 𝑄 ) = 𝑌 ) )
edlemk6.u ⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( ( 𝑠 ‘ ℎ ) = ℎ , 𝑔 , 𝑋 ) )
Assertion erngdvlem4 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 ernggrp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 ernggrp.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
3 erngdv.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
4 erngdv.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 erngdv.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 erngdv.p ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
7 erngdv.o ⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8 erngdv.i ⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑎 ‘ 𝑓 ) ) )
9 erngrnglem.m ⊢ + = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑎 ∘ 𝑏 ) )
10 edlemk6.j ⊢ ∨ = ( join ‘ 𝐾 )
11 edlemk6.m ⊢ ∧ = ( meet ‘ 𝐾 )
12 edlemk6.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 edlemk6.p ⊢ 𝑄 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
14 edlemk6.z ⊢ 𝑍 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑏 ) ) ∧ ( ( ℎ ‘ 𝑄 ) ∨ ( 𝑅 ‘ ( 𝑏 ∘ ◡ ( 𝑠 ‘ ℎ ) ) ) ) )
15 edlemk6.y ⊢ 𝑌 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝑏 ) ) ) )
16 edlemk6.x ⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ ( 𝑠 ‘ ℎ ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑔 ) ) → ( 𝑧 ‘ 𝑄 ) = 𝑌 ) )
17 edlemk6.u ⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( ( 𝑠 ‘ ℎ ) = ℎ , 𝑔 , 𝑋 ) )
18 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
19 1 4 5 2 18 erngbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
20 19 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
21 20 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) )
22 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
23 1 4 5 2 22 erngfmul ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( .r ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑎 ∘ 𝑏 ) ) )
24 9 23 eqtr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( .r ‘ 𝐷 ) )
25 24 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → + = ( .r ‘ 𝐷 ) )
26 3 1 4 5 7 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ 𝐸 )
27 26 19 eleqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐷 ) )
28 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
29 1 4 5 2 28 erngfplus ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) ) )
30 6 29 eqtr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑃 = ( +g ‘ 𝐷 ) )
31 30 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0 𝑃 0 ) = ( 0 ( +g ‘ 𝐷 ) 0 ) )
32 3 1 4 5 7 6 tendo0pl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 0 ∈ 𝐸 ) → ( 0 𝑃 0 ) = 0 )
33 26 32 mpdan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0 𝑃 0 ) = 0 )
34 31 33 eqtr3d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0 ( +g ‘ 𝐷 ) 0 ) = 0 )
35 1 2 3 4 5 6 7 8 erngdvlem1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Grp )
36 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
37 18 28 36 isgrpid2 ⊢ ( 𝐷 ∈ Grp → ( ( 0 ∈ ( Base ‘ 𝐷 ) ∧ ( 0 ( +g ‘ 𝐷 ) 0 ) = 0 ) ↔ ( 0g ‘ 𝐷 ) = 0 ) )
38 35 37 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 0 ∈ ( Base ‘ 𝐷 ) ∧ ( 0 ( +g ‘ 𝐷 ) 0 ) = 0 ) ↔ ( 0g ‘ 𝐷 ) = 0 ) )
39 27 34 38 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝐷 ) = 0 )
40 39 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ( 0g ‘ 𝐷 ) )
41 40 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 0 = ( 0g ‘ 𝐷 ) )
42 1 2 3 4 5 6 7 8 9 erngdvlem3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )
43 1 4 5 2 42 erng1lem ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) )
44 43 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) )
45 44 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) )
46 42 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ Ring )
47 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
48 24 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) )
49 47 48 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) )
50 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → 𝑠 ∈ 𝐸 )
51 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → 𝑡 ∈ 𝐸 )
52 1 4 5 2 22 erngmul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
53 47 50 51 52 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
54 49 53 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
55 3 1 4 5 7 tendoconid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 ∘ 𝑡 ) ≠ 0 )
56 55 3adant1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 ∘ 𝑡 ) ≠ 0 )
57 54 56 eqnetrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 + 𝑡 ) ≠ 0 )
58 3 1 4 5 7 tendo1ne0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 0 )
59 58 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) ≠ 0 )
60 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
61 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ℎ ∈ 𝑇 )
62 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) )
63 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml6 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ∈ 𝐸 ∧ ( 𝑈 ‘ ( 𝑠 ‘ ℎ ) ) = ℎ ) )
64 63 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → 𝑈 ∈ 𝐸 )
65 60 61 62 64 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → 𝑈 ∈ 𝐸 )
66 24 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑈 + 𝑠 ) = ( 𝑈 ( .r ‘ 𝐷 ) 𝑠 ) )
67 66 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 + 𝑠 ) = ( 𝑈 ( .r ‘ 𝐷 ) 𝑠 ) )
68 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → 𝑠 ∈ 𝐸 )
69 1 4 5 2 22 erngmul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑈 ( .r ‘ 𝐷 ) 𝑠 ) = ( 𝑈 ∘ 𝑠 ) )
70 60 65 68 69 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ( .r ‘ 𝐷 ) 𝑠 ) = ( 𝑈 ∘ 𝑠 ) )
71 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml8 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
72 71 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
73 67 70 72 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 0 ) ) → ( 𝑈 + 𝑠 ) = ( I ↾ 𝑇 ) )
74 21 25 41 45 46 57 59 65 73 isdrngd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ DivRing )