Metamath Proof Explorer

Theorem fta1blem

Description: Lemma for fta1b . (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses fta1b.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
fta1b.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
fta1b.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
fta1b.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
fta1b.w ⊢ 𝑊 = ( 0g ‘ 𝑅 )
fta1b.z ⊢ 0 = ( 0g ‘ 𝑃 )
fta1blem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
fta1blem.t ⊢ × = ( .r ‘ 𝑅 )
fta1blem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
fta1blem.s ⊢ · = ( ·𝑠 ‘ 𝑃 )
fta1blem.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
fta1blem.2 ⊢ ( 𝜑 → 𝑀 ∈ 𝐾 )
fta1blem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
fta1blem.4 ⊢ ( 𝜑 → ( 𝑀 × 𝑁 ) = 𝑊 )
fta1blem.5 ⊢ ( 𝜑 → 𝑀 ≠ 𝑊 )
fta1blem.6 ⊢ ( 𝜑 → ( ( 𝑀 · 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑀 · 𝑋 ) ) ) )
Assertion fta1blem ( 𝜑 → 𝑁 = 𝑊 )

Proof

Step Hyp Ref Expression
1 fta1b.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 fta1b.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 fta1b.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
4 fta1b.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
5 fta1b.w ⊢ 𝑊 = ( 0g ‘ 𝑅 )
6 fta1b.z ⊢ 0 = ( 0g ‘ 𝑃 )
7 fta1blem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
8 fta1blem.t ⊢ × = ( .r ‘ 𝑅 )
9 fta1blem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
10 fta1blem.s ⊢ · = ( ·𝑠 ‘ 𝑃 )
11 fta1blem.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
12 fta1blem.2 ⊢ ( 𝜑 → 𝑀 ∈ 𝐾 )
13 fta1blem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
14 fta1blem.4 ⊢ ( 𝜑 → ( 𝑀 × 𝑁 ) = 𝑊 )
15 fta1blem.5 ⊢ ( 𝜑 → 𝑀 ≠ 𝑊 )
16 fta1blem.6 ⊢ ( 𝜑 → ( ( 𝑀 · 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑀 · 𝑋 ) ) ) )
17 4 9 7 1 2 11 13 evl1vard ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑁 ) = 𝑁 ) )
18 4 1 7 2 11 13 17 12 10 8 evl1vsd ⊢ ( 𝜑 → ( ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑁 ) = ( 𝑀 × 𝑁 ) ) )
19 18 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑁 ) = ( 𝑀 × 𝑁 ) )
20 19 14 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑁 ) = 𝑊 )
21 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
22 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
23 7 fvexi ⊢ 𝐾 ∈ V
24 23 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
25 4 1 21 7 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
26 11 25 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
27 2 22 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
28 26 27 syl ⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
29 18 simpld ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
30 28 29 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
31 21 7 22 11 24 30 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) : 𝐾 ⟶ 𝐾 )
32 31 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) Fn 𝐾 )
33 fniniseg ⊢ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) Fn 𝐾 → ( 𝑁 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ↔ ( 𝑁 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑁 ) = 𝑊 ) ) )
34 32 33 syl ⊢ ( 𝜑 → ( 𝑁 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ↔ ( 𝑁 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑁 ) = 𝑊 ) ) )
35 13 20 34 mpbir2and ⊢ ( 𝜑 → 𝑁 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
36 fvex ⊢ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ∈ V
37 36 cnvex ⊢ ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ∈ V
38 37 imaex ⊢ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ V
39 38 a1i ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ V )
40 1nn0 ⊢ 1 ∈ ℕ0
41 40 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
42 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
43 11 42 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
44 9 1 2 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
45 43 44 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
46 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
47 46 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
48 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
49 47 48 mulg1 ⊢ ( 𝑋 ∈ 𝐵 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
50 45 49 syl ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
51 50 oveq2d ⊢ ( 𝜑 → ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( 𝑀 · 𝑋 ) )
52 5 7 1 9 10 46 48 coe1tmfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = 𝑀 )
53 43 12 41 52 syl3anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = 𝑀 )
54 1 6 5 coe1z ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 0 ) = ( ℕ0 × { 𝑊 } ) )
55 43 54 syl ⊢ ( 𝜑 → ( coe1 ‘ 0 ) = ( ℕ0 × { 𝑊 } ) )
56 55 fveq1d ⊢ ( 𝜑 → ( ( coe1 ‘ 0 ) ‘ 1 ) = ( ( ℕ0 × { 𝑊 } ) ‘ 1 ) )
57 5 fvexi ⊢ 𝑊 ∈ V
58 57 fvconst2 ⊢ ( 1 ∈ ℕ0 → ( ( ℕ0 × { 𝑊 } ) ‘ 1 ) = 𝑊 )
59 40 58 ax-mp ⊢ ( ( ℕ0 × { 𝑊 } ) ‘ 1 ) = 𝑊
60 56 59 eqtrdi ⊢ ( 𝜑 → ( ( coe1 ‘ 0 ) ‘ 1 ) = 𝑊 )
61 15 53 60 3netr4d ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) ≠ ( ( coe1 ‘ 0 ) ‘ 1 ) )
62 fveq2 ⊢ ( ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 0 → ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = ( coe1 ‘ 0 ) )
63 62 fveq1d ⊢ ( ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 0 → ( ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = ( ( coe1 ‘ 0 ) ‘ 1 ) )
64 63 necon3i ⊢ ( ( ( coe1 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) ≠ ( ( coe1 ‘ 0 ) ‘ 1 ) → ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ≠ 0 )
65 61 64 syl ⊢ ( 𝜑 → ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ≠ 0 )
66 51 65 eqnetrrd ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) ≠ 0 )
67 eldifsn ⊢ ( ( 𝑀 · 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑀 · 𝑋 ) ≠ 0 ) )
68 29 66 67 sylanbrc ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) )
69 68 16 mpd ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑀 · 𝑋 ) ) )
70 51 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = ( 𝐷 ‘ ( 𝑀 · 𝑋 ) ) )
71 3 7 1 9 10 46 48 5 deg1tm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∈ 𝐾 ∧ 𝑀 ≠ 𝑊 ) ∧ 1 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = 1 )
72 43 12 15 41 71 syl121anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 · ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = 1 )
73 70 72 eqtr3d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 · 𝑋 ) ) = 1 )
74 69 73 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ 1 )
75 hashbnd ⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ V ∧ 1 ∈ ℕ0 ∧ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ 1 ) → ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ Fin )
76 39 41 74 75 syl3anc ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ Fin )
77 7 5 ring0cl ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ 𝐾 )
78 43 77 syl ⊢ ( 𝜑 → 𝑊 ∈ 𝐾 )
79 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
80 1 79 7 2 ply1sclf ⊢ ( 𝑅 ∈ Ring → ( algSc ‘ 𝑃 ) : 𝐾 ⟶ 𝐵 )
81 43 80 syl ⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) : 𝐾 ⟶ 𝐵 )
82 81 12 ffvelcdmd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ∈ 𝐵 )
83 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
84 eqid ⊢ ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) = ( .r ‘ ( 𝑅 ↑s 𝐾 ) )
85 2 83 84 rhmmul ⊢ ( ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) ∧ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ( .r ‘ 𝑃 ) 𝑋 ) ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝑋 ) ) )
86 26 82 45 85 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ( .r ‘ 𝑃 ) 𝑋 ) ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝑋 ) ) )
87 1 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
88 11 87 syl ⊢ ( 𝜑 → 𝑃 ∈ AssAlg )
89 1 ply1sca ⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
90 11 89 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
91 90 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
92 7 91 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
93 12 92 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
94 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
95 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
96 79 94 95 2 83 10 asclmul1 ⊢ ( ( 𝑃 ∈ AssAlg ∧ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ( .r ‘ 𝑃 ) 𝑋 ) = ( 𝑀 · 𝑋 ) )
97 88 93 45 96 syl3anc ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ( .r ‘ 𝑃 ) 𝑋 ) = ( 𝑀 · 𝑋 ) )
98 97 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ( .r ‘ 𝑃 ) 𝑋 ) ) = ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) )
99 28 82 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
100 28 45 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
101 21 22 11 24 99 100 8 84 pwsmulrval ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝑋 ) ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ∘f × ( 𝑂 ‘ 𝑋 ) ) )
102 4 1 7 79 evl1sca ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾 ) → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) = ( 𝐾 × { 𝑀 } ) )
103 11 12 102 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) = ( 𝐾 × { 𝑀 } ) )
104 4 9 7 evl1var ⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐾 ) )
105 11 104 syl ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐾 ) )
106 103 105 oveq12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ∘f × ( 𝑂 ‘ 𝑋 ) ) = ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) )
107 101 106 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑀 ) ) ( .r ‘ ( 𝑅 ↑s 𝐾 ) ) ( 𝑂 ‘ 𝑋 ) ) = ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) )
108 86 98 107 3eqtr3d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) = ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) )
109 108 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑊 ) = ( ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) ‘ 𝑊 ) )
110 fnconstg ⊢ ( 𝑀 ∈ 𝐾 → ( 𝐾 × { 𝑀 } ) Fn 𝐾 )
111 12 110 syl ⊢ ( 𝜑 → ( 𝐾 × { 𝑀 } ) Fn 𝐾 )
112 fnresi ⊢ ( I ↾ 𝐾 ) Fn 𝐾
113 112 a1i ⊢ ( 𝜑 → ( I ↾ 𝐾 ) Fn 𝐾 )
114 fnfvof ⊢ ( ( ( ( 𝐾 × { 𝑀 } ) Fn 𝐾 ∧ ( I ↾ 𝐾 ) Fn 𝐾 ) ∧ ( 𝐾 ∈ V ∧ 𝑊 ∈ 𝐾 ) ) → ( ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) ‘ 𝑊 ) = ( ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) × ( ( I ↾ 𝐾 ) ‘ 𝑊 ) ) )
115 111 113 24 78 114 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) ‘ 𝑊 ) = ( ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) × ( ( I ↾ 𝐾 ) ‘ 𝑊 ) ) )
116 fvconst2g ⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝑊 ∈ 𝐾 ) → ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) = 𝑀 )
117 12 78 116 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) = 𝑀 )
118 fvresi ⊢ ( 𝑊 ∈ 𝐾 → ( ( I ↾ 𝐾 ) ‘ 𝑊 ) = 𝑊 )
119 78 118 syl ⊢ ( 𝜑 → ( ( I ↾ 𝐾 ) ‘ 𝑊 ) = 𝑊 )
120 117 119 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) × ( ( I ↾ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑀 × 𝑊 ) )
121 7 8 5 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ) → ( 𝑀 × 𝑊 ) = 𝑊 )
122 43 12 121 syl2anc ⊢ ( 𝜑 → ( 𝑀 × 𝑊 ) = 𝑊 )
123 120 122 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐾 × { 𝑀 } ) ‘ 𝑊 ) × ( ( I ↾ 𝐾 ) ‘ 𝑊 ) ) = 𝑊 )
124 115 123 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐾 × { 𝑀 } ) ∘f × ( I ↾ 𝐾 ) ) ‘ 𝑊 ) = 𝑊 )
125 109 124 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑊 ) = 𝑊 )
126 fniniseg ⊢ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) Fn 𝐾 → ( 𝑊 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ↔ ( 𝑊 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑊 ) = 𝑊 ) ) )
127 32 126 syl ⊢ ( 𝜑 → ( 𝑊 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ↔ ( 𝑊 ∈ 𝐾 ∧ ( ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) ‘ 𝑊 ) = 𝑊 ) ) )
128 78 125 127 mpbir2and ⊢ ( 𝜑 → 𝑊 ∈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
129 128 snssd ⊢ ( 𝜑 → { 𝑊 } ⊆ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
130 hashsng ⊢ ( 𝑊 ∈ 𝐾 → ( ♯ ‘ { 𝑊 } ) = 1 )
131 78 130 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑊 } ) = 1 )
132 ssdomg ⊢ ( ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ V → ( { 𝑊 } ⊆ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) → { 𝑊 } ≼ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
133 38 129 132 mpsyl ⊢ ( 𝜑 → { 𝑊 } ≼ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
134 snfi ⊢ { 𝑊 } ∈ Fin
135 hashdom ⊢ ( ( { 𝑊 } ∈ Fin ∧ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ V ) → ( ( ♯ ‘ { 𝑊 } ) ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ↔ { 𝑊 } ≼ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
136 134 38 135 mp2an ⊢ ( ( ♯ ‘ { 𝑊 } ) ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ↔ { 𝑊 } ≼ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
137 133 136 sylibr ⊢ ( 𝜑 → ( ♯ ‘ { 𝑊 } ) ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
138 131 137 eqbrtrrd ⊢ ( 𝜑 → 1 ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
139 hashcl ⊢ ( ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ Fin → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ∈ ℕ0 )
140 76 139 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ∈ ℕ0 )
141 140 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ∈ ℝ )
142 1re ⊢ 1 ∈ ℝ
143 letri3 ⊢ ( ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) = 1 ↔ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ 1 ∧ 1 ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ) ) )
144 141 142 143 sylancl ⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) = 1 ↔ ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ≤ 1 ∧ 1 ≤ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ) ) )
145 74 138 144 mpbir2and ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) = 1 )
146 131 145 eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑊 } ) = ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
147 hashen ⊢ ( ( { 𝑊 } ∈ Fin ∧ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ Fin ) → ( ( ♯ ‘ { 𝑊 } ) = ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ↔ { 𝑊 } ≈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
148 134 76 147 sylancr ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑊 } ) = ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) ↔ { 𝑊 } ≈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) )
149 146 148 mpbid ⊢ ( 𝜑 → { 𝑊 } ≈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
150 fisseneq ⊢ ( ( ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∈ Fin ∧ { 𝑊 } ⊆ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ∧ { 𝑊 } ≈ ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) ) → { 𝑊 } = ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
151 76 129 149 150 syl3anc ⊢ ( 𝜑 → { 𝑊 } = ( ◡ ( 𝑂 ‘ ( 𝑀 · 𝑋 ) ) “ { 𝑊 } ) )
152 35 151 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ { 𝑊 } )
153 elsni ⊢ ( 𝑁 ∈ { 𝑊 } → 𝑁 = 𝑊 )
154 152 153 syl ⊢ ( 𝜑 → 𝑁 = 𝑊 )