Metamath Proof Explorer


Theorem erngdvlem3

Description: Lemma for eringring . (Contributed by NM, 6-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 + = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑎𝑏 ) )
Assertion erngdvlem3 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 ∈ Ring )

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 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11 1 4 5 2 10 erngbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
12 11 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
13 eqid ( +g𝐷 ) = ( +g𝐷 )
14 1 4 5 2 13 erngfplus ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( +g𝐷 ) = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) )
15 6 14 eqtr4id ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑃 = ( +g𝐷 ) )
16 eqid ( .r𝐷 ) = ( .r𝐷 )
17 1 4 5 2 16 erngfmul ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( .r𝐷 ) = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑎𝑏 ) ) )
18 9 17 eqtr4id ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = ( .r𝐷 ) )
19 1 2 3 4 5 6 7 8 erngdvlem1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 ∈ Grp )
20 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ( .r𝐷 ) 𝑡 ) )
21 20 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ( .r𝐷 ) 𝑡 ) )
22 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸 ) ) → ( 𝑠 ( .r𝐷 ) 𝑡 ) = ( 𝑠𝑡 ) )
23 22 3impb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 ( .r𝐷 ) 𝑡 ) = ( 𝑠𝑡 ) )
24 21 23 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 + 𝑡 ) = ( 𝑠𝑡 ) )
25 1 5 tendococl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠𝑡 ) ∈ 𝐸 )
26 24 25 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 + 𝑡 ) ∈ 𝐸 )
27 coass ( ( 𝑠𝑡 ) ∘ 𝑢 ) = ( 𝑠 ∘ ( 𝑡𝑢 ) )
28 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 𝑠 + 𝑡 ) + 𝑢 ) = ( ( 𝑠 + 𝑡 ) ( .r𝐷 ) 𝑢 ) )
29 28 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) + 𝑢 ) = ( ( 𝑠 + 𝑡 ) ( .r𝐷 ) 𝑢 ) )
30 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
31 26 3adant3r3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + 𝑡 ) ∈ 𝐸 )
32 simpr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → 𝑢𝐸 )
33 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠 + 𝑡 ) ∈ 𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) ( .r𝐷 ) 𝑢 ) = ( ( 𝑠 + 𝑡 ) ∘ 𝑢 ) )
34 30 31 32 33 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) ( .r𝐷 ) 𝑢 ) = ( ( 𝑠 + 𝑡 ) ∘ 𝑢 ) )
35 18 oveqdr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + 𝑡 ) = ( 𝑠 ( .r𝐷 ) 𝑡 ) )
36 22 3adantr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ( .r𝐷 ) 𝑡 ) = ( 𝑠𝑡 ) )
37 35 36 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + 𝑡 ) = ( 𝑠𝑡 ) )
38 37 coeq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) ∘ 𝑢 ) = ( ( 𝑠𝑡 ) ∘ 𝑢 ) )
39 29 34 38 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) + 𝑢 ) = ( ( 𝑠𝑡 ) ∘ 𝑢 ) )
40 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑠 + ( 𝑡 + 𝑢 ) ) = ( 𝑠 ( .r𝐷 ) ( 𝑡 + 𝑢 ) ) )
41 40 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + ( 𝑡 + 𝑢 ) ) = ( 𝑠 ( .r𝐷 ) ( 𝑡 + 𝑢 ) ) )
42 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → 𝑠𝐸 )
43 18 oveqdr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 + 𝑢 ) = ( 𝑡 ( .r𝐷 ) 𝑢 ) )
44 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 ( .r𝐷 ) 𝑢 ) = ( 𝑡𝑢 ) )
45 44 3adantr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 ( .r𝐷 ) 𝑢 ) = ( 𝑡𝑢 ) )
46 43 45 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 + 𝑢 ) = ( 𝑡𝑢 ) )
47 1 5 tendococl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑡𝐸𝑢𝐸 ) → ( 𝑡𝑢 ) ∈ 𝐸 )
48 47 3adant3r1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡𝑢 ) ∈ 𝐸 )
49 46 48 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 + 𝑢 ) ∈ 𝐸 )
50 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸 ∧ ( 𝑡 + 𝑢 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r𝐷 ) ( 𝑡 + 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡 + 𝑢 ) ) )
51 30 42 49 50 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ( .r𝐷 ) ( 𝑡 + 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡 + 𝑢 ) ) )
52 46 coeq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ∘ ( 𝑡 + 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡𝑢 ) ) )
53 41 51 52 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + ( 𝑡 + 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡𝑢 ) ) )
54 27 39 53 3eqtr4a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) + 𝑢 ) = ( 𝑠 + ( 𝑡 + 𝑢 ) ) )
55 1 4 5 6 tendodi1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ∘ ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑠𝑡 ) 𝑃 ( 𝑠𝑢 ) ) )
56 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑠 + ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ( .r𝐷 ) ( 𝑡 𝑃 𝑢 ) ) )
57 56 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ( .r𝐷 ) ( 𝑡 𝑃 𝑢 ) ) )
58 1 4 5 6 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑡𝐸𝑢𝐸 ) → ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 )
59 58 3adant3r1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 )
60 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸 ∧ ( 𝑡 𝑃 𝑢 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r𝐷 ) ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡 𝑃 𝑢 ) ) )
61 30 42 59 60 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ( .r𝐷 ) ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡 𝑃 𝑢 ) ) )
62 57 61 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + ( 𝑡 𝑃 𝑢 ) ) = ( 𝑠 ∘ ( 𝑡 𝑃 𝑢 ) ) )
63 18 oveqdr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + 𝑢 ) = ( 𝑠 ( .r𝐷 ) 𝑢 ) )
64 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑢𝐸 ) ) → ( 𝑠 ( .r𝐷 ) 𝑢 ) = ( 𝑠𝑢 ) )
65 64 3adantr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 ( .r𝐷 ) 𝑢 ) = ( 𝑠𝑢 ) )
66 63 65 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + 𝑢 ) = ( 𝑠𝑢 ) )
67 37 66 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑡 ) 𝑃 ( 𝑠 + 𝑢 ) ) = ( ( 𝑠𝑡 ) 𝑃 ( 𝑠𝑢 ) ) )
68 55 62 67 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 + ( 𝑡 𝑃 𝑢 ) ) = ( ( 𝑠 + 𝑡 ) 𝑃 ( 𝑠 + 𝑢 ) ) )
69 1 4 5 6 tendodi2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) ∘ 𝑢 ) = ( ( 𝑠𝑢 ) 𝑃 ( 𝑡𝑢 ) ) )
70 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 𝑠 𝑃 𝑡 ) + 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ( .r𝐷 ) 𝑢 ) )
71 70 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) + 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ( .r𝐷 ) 𝑢 ) )
72 1 4 5 6 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 𝑃 𝑡 ) ∈ 𝐸 )
73 72 3adant3r3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( 𝑠 𝑃 𝑡 ) ∈ 𝐸 )
74 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠 𝑃 𝑡 ) ∈ 𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) ( .r𝐷 ) 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ∘ 𝑢 ) )
75 30 73 32 74 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) ( .r𝐷 ) 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ∘ 𝑢 ) )
76 71 75 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) + 𝑢 ) = ( ( 𝑠 𝑃 𝑡 ) ∘ 𝑢 ) )
77 66 46 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 + 𝑢 ) 𝑃 ( 𝑡 + 𝑢 ) ) = ( ( 𝑠𝑢 ) 𝑃 ( 𝑡𝑢 ) ) )
78 69 76 77 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑢𝐸 ) ) → ( ( 𝑠 𝑃 𝑡 ) + 𝑢 ) = ( ( 𝑠 + 𝑢 ) 𝑃 ( 𝑡 + 𝑢 ) ) )
79 1 4 5 tendoidcl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
80 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( I ↾ 𝑇 ) + 𝑠 ) = ( ( I ↾ 𝑇 ) ( .r𝐷 ) 𝑠 ) )
81 80 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( ( I ↾ 𝑇 ) + 𝑠 ) = ( ( I ↾ 𝑇 ) ( .r𝐷 ) 𝑠 ) )
82 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
83 79 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
84 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → 𝑠𝐸 )
85 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸𝑠𝐸 ) ) → ( ( I ↾ 𝑇 ) ( .r𝐷 ) 𝑠 ) = ( ( I ↾ 𝑇 ) ∘ 𝑠 ) )
86 82 83 84 85 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( ( I ↾ 𝑇 ) ( .r𝐷 ) 𝑠 ) = ( ( I ↾ 𝑇 ) ∘ 𝑠 ) )
87 1 4 5 tendo1mul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑠 ) = 𝑠 )
88 81 86 87 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( ( I ↾ 𝑇 ) + 𝑠 ) = 𝑠 )
89 18 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑠 + ( I ↾ 𝑇 ) ) = ( 𝑠 ( .r𝐷 ) ( I ↾ 𝑇 ) ) )
90 89 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( 𝑠 + ( I ↾ 𝑇 ) ) = ( 𝑠 ( .r𝐷 ) ( I ↾ 𝑇 ) ) )
91 1 4 5 2 16 erngmul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( 𝑠 ( .r𝐷 ) ( I ↾ 𝑇 ) ) = ( 𝑠 ∘ ( I ↾ 𝑇 ) ) )
92 82 84 83 91 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( 𝑠 ( .r𝐷 ) ( I ↾ 𝑇 ) ) = ( 𝑠 ∘ ( I ↾ 𝑇 ) ) )
93 1 4 5 tendo1mulr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( 𝑠 ∘ ( I ↾ 𝑇 ) ) = 𝑠 )
94 90 92 93 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸 ) → ( 𝑠 + ( I ↾ 𝑇 ) ) = 𝑠 )
95 12 15 18 19 26 54 68 78 79 88 94 isringd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 ∈ Ring )