Metamath Proof Explorer


Theorem prodmolem2a

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 F = k if k A B 1
prodmo.2 φ k A B
prodmo.3 G = j f j / k B
prodmolem2.4 H = j K j / k B
prodmolem2.5 φ N
prodmolem2.6 φ M
prodmolem2.7 φ A M
prodmolem2.8 φ f : 1 N 1-1 onto A
prodmolem2.9 φ K Isom < , < 1 A A
Assertion prodmolem2a φ seq M × F seq 1 × G N

Proof

Step Hyp Ref Expression
1 prodmo.1 F = k if k A B 1
2 prodmo.2 φ k A B
3 prodmo.3 G = j f j / k B
4 prodmolem2.4 H = j K j / k B
5 prodmolem2.5 φ N
6 prodmolem2.6 φ M
7 prodmolem2.7 φ A M
8 prodmolem2.8 φ f : 1 N 1-1 onto A
9 prodmolem2.9 φ K Isom < , < 1 A A
10 fzfid φ 1 N Fin
11 10 8 hasheqf1od φ 1 N = A
12 5 nnnn0d φ N 0
13 hashfz1 N 0 1 N = N
14 12 13 syl φ 1 N = N
15 11 14 eqtr3d φ A = N
16 15 oveq2d φ 1 A = 1 N
17 isoeq4 1 A = 1 N K Isom < , < 1 A A K Isom < , < 1 N A
18 16 17 syl φ K Isom < , < 1 A A K Isom < , < 1 N A
19 9 18 mpbid φ K Isom < , < 1 N A
20 isof1o K Isom < , < 1 N A K : 1 N 1-1 onto A
21 f1of K : 1 N 1-1 onto A K : 1 N A
22 19 20 21 3syl φ K : 1 N A
23 nnuz = 1
24 5 23 eleqtrdi φ N 1
25 eluzfz2 N 1 N 1 N
26 24 25 syl φ N 1 N
27 22 26 ffvelrnd φ K N A
28 7 27 sseldd φ K N M
29 7 sselda φ j A j M
30 19 20 syl φ K : 1 N 1-1 onto A
31 f1ocnvfv2 K : 1 N 1-1 onto A j A K K -1 j = j
32 30 31 sylan φ j A K K -1 j = j
33 f1ocnv K : 1 N 1-1 onto A K -1 : A 1-1 onto 1 N
34 f1of K -1 : A 1-1 onto 1 N K -1 : A 1 N
35 30 33 34 3syl φ K -1 : A 1 N
36 35 ffvelrnda φ j A K -1 j 1 N
37 elfzle2 K -1 j 1 N K -1 j N
38 36 37 syl φ j A K -1 j N
39 19 adantr φ j A K Isom < , < 1 N A
40 fzssuz 1 N 1
41 uzssz 1
42 zssre
43 41 42 sstri 1
44 40 43 sstri 1 N
45 ressxr *
46 44 45 sstri 1 N *
47 46 a1i φ j A 1 N *
48 uzssz M
49 48 42 sstri M
50 49 45 sstri M *
51 7 50 sstrdi φ A *
52 51 adantr φ j A A *
53 26 adantr φ j A N 1 N
54 leisorel K Isom < , < 1 N A 1 N * A * K -1 j 1 N N 1 N K -1 j N K K -1 j K N
55 39 47 52 36 53 54 syl122anc φ j A K -1 j N K K -1 j K N
56 38 55 mpbid φ j A K K -1 j K N
57 32 56 eqbrtrrd φ j A j K N
58 7 48 sstrdi φ A
59 58 sselda φ j A j
60 eluzelz K N M K N
61 28 60 syl φ K N
62 61 adantr φ j A K N
63 eluz j K N K N j j K N
64 59 62 63 syl2anc φ j A K N j j K N
65 57 64 mpbird φ j A K N j
66 elfzuzb j M K N j M K N j
67 29 65 66 sylanbrc φ j A j M K N
68 67 ex φ j A j M K N
69 68 ssrdv φ A M K N
70 1 2 28 69 fprodcvg φ seq M × F seq M × F K N
71 mulid2 m 1 m = m
72 71 adantl φ m 1 m = m
73 mulid1 m m 1 = m
74 73 adantl φ m m 1 = m
75 mulcl m x m x
76 75 adantl φ m x m x
77 1cnd φ 1
78 26 16 eleqtrrd φ N 1 A
79 iftrue k A if k A B 1 = B
80 79 adantl φ k A if k A B 1 = B
81 80 2 eqeltrd φ k A if k A B 1
82 81 ex φ k A if k A B 1
83 iffalse ¬ k A if k A B 1 = 1
84 ax-1cn 1
85 83 84 eqeltrdi ¬ k A if k A B 1
86 82 85 pm2.61d1 φ if k A B 1
87 86 adantr φ k if k A B 1
88 87 1 fmptd φ F :
89 elfzelz m M K A m
90 ffvelrn F : m F m
91 88 89 90 syl2an φ m M K A F m
92 fveqeq2 k = m F k = 1 F m = 1
93 eldifi k M K A A k M K A
94 93 elfzelzd k M K A A k
95 eldifn k M K A A ¬ k A
96 95 83 syl k M K A A if k A B 1 = 1
97 96 84 eqeltrdi k M K A A if k A B 1
98 1 fvmpt2 k if k A B 1 F k = if k A B 1
99 94 97 98 syl2anc k M K A A F k = if k A B 1
100 99 96 eqtrd k M K A A F k = 1
101 92 100 vtoclga m M K A A F m = 1
102 101 adantl φ m M K A A F m = 1
103 isof1o K Isom < , < 1 A A K : 1 A 1-1 onto A
104 f1of K : 1 A 1-1 onto A K : 1 A A
105 9 103 104 3syl φ K : 1 A A
106 105 ffvelrnda φ x 1 A K x A
107 106 iftrued φ x 1 A if K x A K x / k B 1 = K x / k B
108 58 adantr φ x 1 A A
109 108 106 sseldd φ x 1 A K x
110 nfv k φ
111 nfv k K x A
112 nfcsb1v _ k K x / k B
113 nfcv _ k 1
114 111 112 113 nfif _ k if K x A K x / k B 1
115 114 nfel1 k if K x A K x / k B 1
116 110 115 nfim k φ if K x A K x / k B 1
117 fvex K x V
118 eleq1 k = K x k A K x A
119 csbeq1a k = K x B = K x / k B
120 118 119 ifbieq1d k = K x if k A B 1 = if K x A K x / k B 1
121 120 eleq1d k = K x if k A B 1 if K x A K x / k B 1
122 121 imbi2d k = K x φ if k A B 1 φ if K x A K x / k B 1
123 116 117 122 86 vtoclf φ if K x A K x / k B 1
124 123 adantr φ x 1 A if K x A K x / k B 1
125 eleq1 n = K x n A K x A
126 csbeq1 n = K x n / k B = K x / k B
127 125 126 ifbieq1d n = K x if n A n / k B 1 = if K x A K x / k B 1
128 nfcv _ n if k A B 1
129 nfv k n A
130 nfcsb1v _ k n / k B
131 129 130 113 nfif _ k if n A n / k B 1
132 eleq1 k = n k A n A
133 csbeq1a k = n B = n / k B
134 132 133 ifbieq1d k = n if k A B 1 = if n A n / k B 1
135 128 131 134 cbvmpt k if k A B 1 = n if n A n / k B 1
136 1 135 eqtri F = n if n A n / k B 1
137 127 136 fvmptg K x if K x A K x / k B 1 F K x = if K x A K x / k B 1
138 109 124 137 syl2anc φ x 1 A F K x = if K x A K x / k B 1
139 elfznn x 1 A x
140 107 124 eqeltrrd φ x 1 A K x / k B
141 fveq2 j = x K j = K x
142 141 csbeq1d j = x K j / k B = K x / k B
143 142 4 fvmptg x K x / k B H x = K x / k B
144 139 140 143 syl2an2 φ x 1 A H x = K x / k B
145 107 138 144 3eqtr4rd φ x 1 A H x = F K x
146 72 74 76 77 9 78 7 91 102 145 seqcoll φ seq M × F K N = seq 1 × H N
147 5 5 jca φ N N
148 1 2 3 4 147 8 30 prodmolem3 φ seq 1 × G N = seq 1 × H N
149 146 148 eqtr4d φ seq M × F K N = seq 1 × G N
150 70 149 breqtrd φ seq M × F seq 1 × G N