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 )