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