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

Metamath Proof Explorer

Theorem fidomndrnglem

Description: Lemma for fidomndrng . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses fidomndrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
fidomndrng.z ⊢ 0 = ( 0g ‘ 𝑅 )
fidomndrng.o ⊢ 1 = ( 1r ‘ 𝑅 )
fidomndrng.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
fidomndrng.t ⊢ · = ( .r ‘ 𝑅 )
fidomndrng.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
fidomndrng.x ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fidomndrng.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 0 } ) )
fidomndrng.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝐴 ) )
Assertion fidomndrnglem ( 𝜑 → 𝐴 ∥ 1 )

Proof

Step Hyp Ref Expression
1 fidomndrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 fidomndrng.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 fidomndrng.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 fidomndrng.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
5 fidomndrng.t ⊢ · = ( .r ‘ 𝑅 )
6 fidomndrng.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
7 fidomndrng.x ⊢ ( 𝜑 → 𝐵 ∈ Fin )
8 fidomndrng.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 0 } ) )
9 fidomndrng.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝐴 ) )
10 8 eldifad ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
11 eldifsni ⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 0 } ) → 𝐴 ≠ 0 )
12 8 11 syl ⊢ ( 𝜑 → 𝐴 ≠ 0 )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 0 ) → 𝐴 ≠ 0 )
14 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
15 ovex ⊢ ( 𝑦 · 𝐴 ) ∈ V
16 14 9 15 fvmpt ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 𝐴 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 𝐴 ) )
18 17 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = 0 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ Domn )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
21 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
22 1 5 2 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑦 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( 𝑦 = 0 ∨ 𝐴 = 0 ) ) )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( 𝑦 = 0 ∨ 𝐴 = 0 ) ) )
24 18 23 bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = 0 ↔ ( 𝑦 = 0 ∨ 𝐴 = 0 ) ) )
25 24 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 0 ) → ( 𝑦 = 0 ∨ 𝐴 = 0 ) )
26 25 ord ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 0 ) → ( ¬ 𝑦 = 0 → 𝐴 = 0 ) )
27 26 necon1ad ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 0 ) → ( 𝐴 ≠ 0 → 𝑦 = 0 ) )
28 13 27 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 0 ) → 𝑦 = 0 )
29 28 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = 0 → 𝑦 = 0 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 0 → 𝑦 = 0 ) )
31 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
32 6 31 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
33 1 5 ringrghm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝐴 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
34 32 10 33 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝐴 ) ) ∈ ( 𝑅 GrpHom 𝑅 ) )
35 9 34 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑅 ) )
36 1 1 2 2 ghmf1 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑅 ) → ( 𝐹 : 𝐵 –1-1→ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 0 → 𝑦 = 0 ) ) )
37 35 36 syl ⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = 0 → 𝑦 = 0 ) ) )
38 30 37 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐵 )
39 enreffi ⊢ ( 𝐵 ∈ Fin → 𝐵 ≈ 𝐵 )
40 7 39 syl ⊢ ( 𝜑 → 𝐵 ≈ 𝐵 )
41 f1finf1o ⊢ ( ( 𝐵 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐵 –1-1→ 𝐵 ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) )
42 40 7 41 syl2anc ⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ 𝐵 ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) )
43 38 42 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
44 f1ocnv ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
45 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 ⟶ 𝐵 )
46 43 44 45 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 ⟶ 𝐵 )
47 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
48 32 47 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
49 46 48 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 1 ) ∈ 𝐵 )
50 1 4 5 dvdsrmul ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 1 ) ∈ 𝐵 ) → 𝐴 ∥ ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) )
51 10 49 50 syl2anc ⊢ ( 𝜑 → 𝐴 ∥ ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) )
52 oveq1 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 1 ) → ( 𝑦 · 𝐴 ) = ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) )
53 14 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 · 𝐴 ) )
54 9 53 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 · 𝐴 ) )
55 ovex ⊢ ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) ∈ V
56 52 54 55 fvmpt ⊢ ( ( ◡ 𝐹 ‘ 1 ) ∈ 𝐵 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 1 ) ) = ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) )
57 49 56 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 1 ) ) = ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) )
58 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 1 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 1 ) ) = 1 )
59 43 48 58 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 1 ) ) = 1 )
60 57 59 eqtr3d ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 1 ) · 𝐴 ) = 1 )
61 51 60 breqtrd ⊢ ( 𝜑 → 𝐴 ∥ 1 )