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

Metamath Proof Explorer

Theorem lflnegcl

Description: Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp , and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014)

Ref Expression
Hypotheses lflnegcl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflnegcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
lflnegcl.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
lflnegcl.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) )
lflnegcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lflnegcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lflnegcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lflnegcl ( 𝜑 → 𝑁 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 lflnegcl.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lflnegcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 lflnegcl.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
4 lflnegcl.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) )
5 lflnegcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lflnegcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lflnegcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
9 6 8 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
11 9 10 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑅 ∈ Grp )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ LMod )
14 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝐺 ∈ 𝐹 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
16 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 2 16 1 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
18 13 14 15 17 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
19 16 3 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
20 12 18 19 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
21 20 4 fmptd ⊢ ( 𝜑 → 𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
22 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
23 9 22 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑅 ∈ Abel )
25 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑅 ∈ Ring )
26 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑘 ∈ ( Base ‘ 𝑅 ) )
27 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
28 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 )
29 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
30 2 16 1 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
31 27 28 29 30 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
32 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33 16 32 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
34 25 26 31 33 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
35 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
36 2 16 1 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
37 27 28 35 36 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
38 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
39 16 38 3 ablinvadd ⊢ ( ( 𝑅 ∈ Abel ∧ ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
40 24 34 37 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐼 ‘ ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
41 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
42 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
43 1 41 2 42 16 38 32 5 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
44 27 28 26 29 35 43 syl113anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
45 44 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) = ( 𝐼 ‘ ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) ) )
46 16 32 3 25 26 31 ringmneg2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝐼 ‘ ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ) )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( ( 𝐼 ‘ ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
48 40 45 47 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
49 1 2 42 16 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
50 27 26 29 49 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
51 1 41 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
52 27 50 35 51 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
53 2fveq3 ⊢ ( 𝑥 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) )
54 fvex ⊢ ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) ∈ V
55 53 4 54 fvmpt ⊢ ( ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) )
56 52 55 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) ) )
57 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) )
58 fvex ⊢ ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ V
59 57 4 58 fvmpt ⊢ ( 𝑦 ∈ 𝑉 → ( 𝑁 ‘ 𝑦 ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) )
60 29 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑁 ‘ 𝑦 ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) )
61 60 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) = ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
62 2fveq3 ⊢ ( 𝑥 = 𝑧 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) )
63 fvex ⊢ ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ V
64 62 4 63 fvmpt ⊢ ( 𝑧 ∈ 𝑉 → ( 𝑁 ‘ 𝑧 ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) )
65 35 64 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑁 ‘ 𝑧 ) = ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) )
66 61 65 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( 𝐼 ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
67 48 56 66 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝑧 ) ) )
68 67 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝑧 ) ) )
69 1 41 2 42 16 38 32 5 islfl ⊢ ( 𝑊 ∈ LMod → ( 𝑁 ∈ 𝐹 ↔ ( 𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝑧 ) ) ) ) )
70 6 69 syl ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐹 ↔ ( 𝑁 : 𝑉 ⟶ ( Base ‘ 𝑅 ) ∧ ∀ 𝑘 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝑉 ∀ 𝑧 ∈ 𝑉 ( 𝑁 ‘ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑘 ( .r ‘ 𝑅 ) ( 𝑁 ‘ 𝑦 ) ) ( +g ‘ 𝑅 ) ( 𝑁 ‘ 𝑧 ) ) ) ) )
71 21 68 70 mpbir2and ⊢ ( 𝜑 → 𝑁 ∈ 𝐹 )