Metamath Proof Explorer

Theorem erng1lem

Description: Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013)

Ref Expression
Hypotheses erng1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
erng1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erng1.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erng1.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
erng1.r ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )
Assertion erng1lem ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 erng1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 erng1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erng1.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erng1.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
5 erng1.r ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )
6 1 2 3 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
7 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 1 2 3 4 7 erngbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
9 6 8 eleqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) )
10 8 eleq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ ( Base ‘ 𝐷 ) ↔ 𝑢 ∈ 𝐸 ) )
11 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 6 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
13 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → 𝑢 ∈ 𝐸 )
14 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
15 1 2 3 4 14 erngmul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( ( I ↾ 𝑇 ) ∘ 𝑢 ) )
16 11 12 13 15 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = ( ( I ↾ 𝑇 ) ∘ 𝑢 ) )
17 1 2 3 tendo1mul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑢 ) = 𝑢 )
18 16 17 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 )
19 1 2 3 4 14 erngmul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ 𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( 𝑢 ∘ ( I ↾ 𝑇 ) ) )
20 11 13 12 19 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( 𝑢 ∘ ( I ↾ 𝑇 ) ) )
21 1 2 3 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ∘ ( I ↾ 𝑇 ) ) = 𝑢 )
22 20 21 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 )
23 18 22 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) )
24 23 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ 𝐸 → ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) )
25 10 24 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ ( Base ‘ 𝐷 ) → ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) )
26 25 ralrimiv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) )
27 eqid ⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 )
28 7 14 27 isringid ⊢ ( 𝐷 ∈ Ring → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
29 5 28 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
30 9 26 29 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) )