Metamath Proof Explorer

Theorem abvcxp

Description: Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvcxp.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvcxp.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
abvcxp.f ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) )
Assertion abvcxp ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝐺 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 abvcxp.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvcxp.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 abvcxp.f ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) )
4 1 a1i ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝐴 = ( AbsVal ‘ 𝑅 ) )
5 2 a1i ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝐵 = ( Base ‘ 𝑅 ) )
6 eqidd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
7 eqidd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) )
8 eqidd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
9 1 abvrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
10 9 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝑅 ∈ Ring )
11 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
12 11 adantlr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
13 1 2 abvge0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
14 13 adantlr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
15 0xr ⊢ 0 ∈ ℝ*
16 1re ⊢ 1 ∈ ℝ
17 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑆 ∈ ( 0 (,] 1 ) ↔ ( 𝑆 ∈ ℝ ∧ 0 < 𝑆 ∧ 𝑆 ≤ 1 ) ) )
18 15 16 17 mp2an ⊢ ( 𝑆 ∈ ( 0 (,] 1 ) ↔ ( 𝑆 ∈ ℝ ∧ 0 < 𝑆 ∧ 𝑆 ≤ 1 ) )
19 18 bilani ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 𝑆 ∈ ℝ ∧ 0 < 𝑆 ∧ 𝑆 ≤ 1 ) )
20 19 simp1d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝑆 ∈ ℝ )
21 20 adantr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ∈ ℝ )
22 12 14 21 recxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) ∈ ℝ )
23 22 3 fmptd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝐺 : 𝐵 ⟶ ℝ )
24 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
25 2 24 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
26 10 25 syl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
27 fveq2 ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
28 27 oveq1d ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) = ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) )
29 ovex ⊢ ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) ∈ V
30 28 3 29 fvmpt ⊢ ( ( 0g ‘ 𝑅 ) ∈ 𝐵 → ( 𝐺 ‘ ( 0g ‘ 𝑅 ) ) = ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) )
31 26 30 syl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑅 ) ) = ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) )
32 1 24 abv0 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = 0 )
33 32 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = 0 )
34 33 oveq1d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) = ( 0 ↑𝑐 𝑆 ) )
35 20 recnd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝑆 ∈ ℂ )
36 19 simp2d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 0 < 𝑆 )
37 36 gt0ne0d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝑆 ≠ 0 )
38 35 37 0cxpd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 0 ↑𝑐 𝑆 ) = 0 )
39 34 38 eqtrd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ↑𝑐 𝑆 ) = 0 )
40 31 39 eqtrd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑅 ) ) = 0 )
41 simp1l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 𝐹 ∈ 𝐴 )
42 simp2 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ 𝐵 )
43 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
44 41 42 43 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
45 1 2 24 abvgt0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( 𝐹 ‘ 𝑦 ) )
46 45 3adant1r ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( 𝐹 ‘ 𝑦 ) )
47 44 46 elrpd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ+ )
48 20 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 𝑆 ∈ ℝ )
49 47 48 rpcxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) ∈ ℝ+ )
50 49 rpgt0d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) )
51 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
52 51 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) = ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) )
53 ovex ⊢ ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) ∈ V
54 52 3 53 fvmpt ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐺 ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) )
55 42 54 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) )
56 50 55 breqtrrd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( 𝐺 ‘ 𝑦 ) )
57 simp1l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝐹 ∈ 𝐴 )
58 simp2l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑦 ∈ 𝐵 )
59 simp3l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑧 ∈ 𝐵 )
60 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
61 1 2 60 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
62 57 58 59 61 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
63 62 oveq1d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) = ( ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) )
64 57 58 43 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
65 1 2 abvge0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
66 57 58 65 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑦 ) )
67 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
68 57 59 67 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
69 1 2 abvge0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
70 57 59 69 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑧 ) )
71 35 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑆 ∈ ℂ )
72 64 66 68 70 71 mulcxpd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) = ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) · ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
73 63 72 eqtrd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) = ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) · ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
74 10 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
75 2 60 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
76 74 58 59 75 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
77 fveq2 ⊢ ( 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
78 77 oveq1d ⊢ ( 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) = ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
79 ovex ⊢ ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ∈ V
80 78 3 79 fvmpt ⊢ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 → ( 𝐺 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
81 76 80 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
82 58 54 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) )
83 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
84 83 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) = ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) )
85 ovex ⊢ ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ∈ V
86 84 3 85 fvmpt ⊢ ( 𝑧 ∈ 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) )
87 59 86 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) )
88 82 87 oveq12d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) · ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
89 73 81 88 3eqtr4d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐺 ‘ 𝑦 ) · ( 𝐺 ‘ 𝑧 ) ) )
90 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
91 74 90 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑅 ∈ Grp )
92 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
93 2 92 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
94 91 58 59 93 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
95 1 2 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ∈ ℝ )
96 57 94 95 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ∈ ℝ )
97 1 2 abvge0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
98 57 94 97 syl2anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 0 ≤ ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
99 19 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑆 ∈ ℝ ∧ 0 < 𝑆 ∧ 𝑆 ≤ 1 ) )
100 99 simp1d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑆 ∈ ℝ )
101 96 98 100 recxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ∈ ℝ )
102 64 68 readdcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
103 64 68 66 70 addge0d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) )
104 102 103 100 recxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) ∈ ℝ )
105 64 66 100 recxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) ∈ ℝ )
106 68 70 100 recxpcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ∈ ℝ )
107 105 106 readdcld ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) + ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) ∈ ℝ )
108 1 2 92 abvtri ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) )
109 57 58 59 108 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) )
110 99 simp2d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 0 < 𝑆 )
111 100 110 elrpd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑆 ∈ ℝ+ )
112 96 98 102 103 111 cxple2d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ↔ ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ≤ ( ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) ) )
113 109 112 mpbid ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ≤ ( ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) )
114 99 simp3d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑆 ≤ 1 )
115 64 66 68 70 111 114 cxpaddle ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ↑𝑐 𝑆 ) ≤ ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) + ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
116 101 104 107 113 115 letrd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ≤ ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) + ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
117 fveq2 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
118 117 oveq1d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ↑𝑐 𝑆 ) = ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
119 ovex ⊢ ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) ∈ V
120 118 3 119 fvmpt ⊢ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 → ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
121 94 120 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ↑𝑐 𝑆 ) )
122 82 87 oveq12d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐺 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑦 ) ↑𝑐 𝑆 ) + ( ( 𝐹 ‘ 𝑧 ) ↑𝑐 𝑆 ) ) )
123 116 121 122 3brtr4d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐺 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐺 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑧 ) ) )
124 4 5 6 7 8 10 23 40 56 89 123 isabvd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑆 ∈ ( 0 (,] 1 ) ) → 𝐺 ∈ 𝐴 )