Metamath Proof Explorer

Theorem ablfac1eulem

Description: Lemma for ablfac1eu . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses ablfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
ablfac1c.d ⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
ablfac1.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
ablfac1eu.1 ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝐵 ) )
ablfac1eu.2 ⊢ ( 𝜑 → dom 𝑇 = 𝐴 )
ablfac1eu.3 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℕ0 )
ablfac1eu.4 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
ablfac1eulem.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
ablfac1eulem.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion ablfac1eulem ( 𝜑 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ablfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
4 ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
6 ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
7 ablfac1c.d ⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
8 ablfac1.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
9 ablfac1eu.1 ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝐵 ) )
10 ablfac1eu.2 ⊢ ( 𝜑 → dom 𝑇 = 𝐴 )
11 ablfac1eu.3 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℕ0 )
12 ablfac1eu.4 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
13 ablfac1eulem.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
14 ablfac1eulem.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
15 ssid ⊢ 𝐴 ⊆ 𝐴
16 sseq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
17 difeq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∖ { 𝑃 } ) = ( ∅ ∖ { 𝑃 } ) )
18 0dif ⊢ ( ∅ ∖ { 𝑃 } ) = ∅
19 17 18 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑦 ∖ { 𝑃 } ) = ∅ )
20 19 reseq2d ⊢ ( 𝑦 = ∅ → ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ∅ ) )
21 res0 ⊢ ( 𝑇 ↾ ∅ ) = ∅
22 20 21 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) = ∅ )
23 22 oveq2d ⊢ ( 𝑦 = ∅ → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ∅ ) )
24 23 fveq2d ⊢ ( 𝑦 = ∅ → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ∅ ) ) )
25 24 breq2d ⊢ ( 𝑦 = ∅ → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ) )
26 25 notbid ⊢ ( 𝑦 = ∅ → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ) )
27 16 26 imbi12d ⊢ ( 𝑦 = ∅ → ( ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ↔ ( ∅ ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ) ) )
28 27 imbi2d ⊢ ( 𝑦 = ∅ → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ) ) ) )
29 sseq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
30 difeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∖ { 𝑃 } ) = ( 𝑧 ∖ { 𝑃 } ) )
31 30 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) )
32 31 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) )
33 32 fveq2d ⊢ ( 𝑦 = 𝑧 → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) )
34 33 breq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
35 34 notbid ⊢ ( 𝑦 = 𝑧 → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
36 29 35 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ↔ ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) ) )
37 36 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) ) ) )
38 sseq1 ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( 𝑦 ⊆ 𝐴 ↔ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) )
39 difeq1 ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( 𝑦 ∖ { 𝑃 } ) = ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
40 39 reseq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) )
41 40 oveq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) )
42 41 fveq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) )
43 42 breq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) )
44 43 notbid ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) )
45 38 44 imbi12d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ↔ ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) )
46 45 imbi2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑞 } ) → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) ) )
47 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
48 difeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∖ { 𝑃 } ) = ( 𝐴 ∖ { 𝑃 } ) )
49 48 reseq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) )
50 49 oveq2d ⊢ ( 𝑦 = 𝐴 → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) )
51 50 fveq2d ⊢ ( 𝑦 = 𝐴 → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) )
52 51 breq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) )
53 52 notbid ⊢ ( 𝑦 = 𝐴 → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ↔ ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) )
54 47 53 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ↔ ( 𝐴 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) ) )
55 54 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → ( 𝑦 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑦 ∖ { 𝑃 } ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) ) ) )
56 nprmdvds1 ⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1 )
57 13 56 syl ⊢ ( 𝜑 → ¬ 𝑃 ∥ 1 )
58 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
59 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
60 59 dprd0 ⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
61 4 58 60 3syl ⊢ ( 𝜑 → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
62 61 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } )
63 62 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐺 DProd ∅ ) ) = ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) )
64 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
65 hashsng ⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 )
66 64 65 ax-mp ⊢ ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1
67 63 66 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐺 DProd ∅ ) ) = 1 )
68 67 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ↔ 𝑃 ∥ 1 ) )
69 57 68 mtbird ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) )
70 69 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ∅ ) ) ) )
71 ssun1 ⊢ 𝑧 ⊆ ( 𝑧 ∪ { 𝑞 } )
72 sstr ⊢ ( ( 𝑧 ⊆ ( 𝑧 ∪ { 𝑞 } ) ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) → 𝑧 ⊆ 𝐴 )
73 71 72 mpan ⊢ ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → 𝑧 ⊆ 𝐴 )
74 73 imim1i ⊢ ( ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
75 9 simpld ⊢ ( 𝜑 → 𝐺 dom DProd 𝑇 )
76 75 10 dprdf2 ⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
77 76 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝑇 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
78 simprr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 )
79 78 ssdifssd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ⊆ 𝐴 )
80 77 79 fssresd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) : ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ⟶ ( SubGrp ‘ 𝐺 ) )
81 simprl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ¬ 𝑞 ∈ 𝑧 )
82 disjsn ⊢ ( ( 𝑧 ∩ { 𝑞 } ) = ∅ ↔ ¬ 𝑞 ∈ 𝑧 )
83 81 82 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑧 ∩ { 𝑞 } ) = ∅ )
84 83 difeq1d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑧 ∩ { 𝑞 } ) ∖ { 𝑃 } ) = ( ∅ ∖ { 𝑃 } ) )
85 difindir ⊢ ( ( 𝑧 ∩ { 𝑞 } ) ∖ { 𝑃 } ) = ( ( 𝑧 ∖ { 𝑃 } ) ∩ ( { 𝑞 } ∖ { 𝑃 } ) )
86 84 85 18 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑧 ∖ { 𝑃 } ) ∩ ( { 𝑞 } ∖ { 𝑃 } ) ) = ∅ )
87 difundir ⊢ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) = ( ( 𝑧 ∖ { 𝑃 } ) ∪ ( { 𝑞 } ∖ { 𝑃 } ) )
88 87 a1i ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) = ( ( 𝑧 ∖ { 𝑃 } ) ∪ ( { 𝑞 } ∖ { 𝑃 } ) ) )
89 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
90 75 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐺 dom DProd 𝑇 )
91 10 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → dom 𝑇 = 𝐴 )
92 90 91 79 dprdres ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 dom DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ∧ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ⊆ ( 𝐺 DProd 𝑇 ) ) )
93 92 simpld ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐺 dom DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) )
94 80 86 88 89 93 dprdsplit ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) = ( ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
95 94 fveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) )
96 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
97 80 fdmd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → dom ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) = ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
98 ssdif ⊢ ( 𝑧 ⊆ ( 𝑧 ∪ { 𝑞 } ) → ( 𝑧 ∖ { 𝑃 } ) ⊆ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
99 71 98 mp1i ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑧 ∖ { 𝑃 } ) ⊆ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
100 93 97 99 dprdres ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ∧ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) )
101 100 simpld ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) )
102 dprdsubg ⊢ ( 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
103 101 102 syl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
104 ssun2 ⊢ { 𝑞 } ⊆ ( 𝑧 ∪ { 𝑞 } )
105 ssdif ⊢ ( { 𝑞 } ⊆ ( 𝑧 ∪ { 𝑞 } ) → ( { 𝑞 } ∖ { 𝑃 } ) ⊆ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
106 104 105 mp1i ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( { 𝑞 } ∖ { 𝑃 } ) ⊆ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) )
107 93 97 106 dprdres ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ∧ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) )
108 107 simpld ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) )
109 dprdsubg ⊢ ( 𝐺 dom DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
110 108 109 syl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
111 93 97 99 106 86 59 dprddisj2 ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∩ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
112 93 97 99 106 86 96 dprdcntz2 ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
113 5 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐵 ∈ Fin )
114 1 dprdssv ⊢ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ 𝐵
115 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ Fin )
116 113 114 115 sylancl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ Fin )
117 1 dprdssv ⊢ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ⊆ 𝐵
118 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ Fin )
119 113 117 118 sylancl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ Fin )
120 89 59 96 103 110 111 112 116 119 lsmhash ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) = ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) )
121 99 resabs1d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) )
122 121 oveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) )
123 122 fveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) )
124 106 resabs1d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) )
125 124 oveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) )
126 125 fveq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
127 123 126 oveq12d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) = ( ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) )
128 95 120 127 3eqtrd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) = ( ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) )
129 128 breq2d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ) )
130 13 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝑃 ∈ ℙ )
131 1 dprdssv ⊢ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ 𝐵
132 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ Fin )
133 113 131 132 sylancl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ Fin )
134 hashcl ⊢ ( ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∈ ℕ0 )
135 133 134 syl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∈ ℕ0 )
136 135 nn0zd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∈ ℤ )
137 1 dprdssv ⊢ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ⊆ 𝐵
138 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ Fin )
139 113 137 138 sylancl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ Fin )
140 hashcl ⊢ ( ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ∈ ℕ0 )
141 139 140 syl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ∈ ℕ0 )
142 141 nn0zd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ∈ ℤ )
143 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∈ ℤ ∧ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ↔ ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∨ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ) )
144 130 136 142 143 syl3anc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ↔ ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∨ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ) )
145 129 144 bitrd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ↔ ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∨ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) ) )
146 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ¬ 𝑃 ∥ 1 )
147 simpr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → 𝑞 = 𝑃 )
148 147 sneqd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → { 𝑞 } = { 𝑃 } )
149 148 difeq1d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( { 𝑞 } ∖ { 𝑃 } ) = ( { 𝑃 } ∖ { 𝑃 } ) )
150 difid ⊢ ( { 𝑃 } ∖ { 𝑃 } ) = ∅
151 149 150 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( { 𝑞 } ∖ { 𝑃 } ) = ∅ )
152 151 reseq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) = ( 𝑇 ↾ ∅ ) )
153 152 21 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) = ∅ )
154 153 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) = ( 𝐺 DProd ∅ ) )
155 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } )
156 154 155 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) = { ( 0g ‘ 𝐺 ) } )
157 156 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) )
158 157 66 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = 1 )
159 158 breq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ 1 ) )
160 146 159 mtbird ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 = 𝑃 ) → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
161 6 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐴 ⊆ ℙ )
162 78 unssbd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → { 𝑞 } ⊆ 𝐴 )
163 vex ⊢ 𝑞 ∈ V
164 163 snss ⊢ ( 𝑞 ∈ 𝐴 ↔ { 𝑞 } ⊆ 𝐴 )
165 162 164 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝑞 ∈ 𝐴 )
166 161 165 sseldd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝑞 ∈ ℙ )
167 165 11 syldan ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → 𝐶 ∈ ℕ0 )
168 prmdvdsexpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝐶 ∈ ℕ0 ) → ( 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) → 𝑃 = 𝑞 ) )
169 130 166 167 168 syl3anc ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) → 𝑃 = 𝑞 ) )
170 eqcom ⊢ ( 𝑃 = 𝑞 ↔ 𝑞 = 𝑃 )
171 169 170 syl6ib ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) → 𝑞 = 𝑃 ) )
172 171 necon3ad ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑞 ≠ 𝑃 → ¬ 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) ) )
173 172 imp ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ¬ 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) )
174 disjsn2 ⊢ ( 𝑞 ≠ 𝑃 → ( { 𝑞 } ∩ { 𝑃 } ) = ∅ )
175 174 adantl ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( { 𝑞 } ∩ { 𝑃 } ) = ∅ )
176 disj3 ⊢ ( ( { 𝑞 } ∩ { 𝑃 } ) = ∅ ↔ { 𝑞 } = ( { 𝑞 } ∖ { 𝑃 } ) )
177 175 176 sylib ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → { 𝑞 } = ( { 𝑞 } ∖ { 𝑃 } ) )
178 177 reseq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝑇 ↾ { 𝑞 } ) = ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) )
179 178 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝐺 DProd ( 𝑇 ↾ { 𝑞 } ) ) = ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) )
180 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → 𝐺 dom DProd 𝑇 )
181 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → dom 𝑇 = 𝐴 )
182 165 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → 𝑞 ∈ 𝐴 )
183 180 181 182 dpjlem ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝐺 DProd ( 𝑇 ↾ { 𝑞 } ) ) = ( 𝑇 ‘ 𝑞 ) )
184 179 183 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) = ( 𝑇 ‘ 𝑞 ) )
185 184 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) )
186 165 12 syldan ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
188 185 187 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) = ( 𝑞 ↑ 𝐶 ) )
189 188 breq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ↔ 𝑃 ∥ ( 𝑞 ↑ 𝐶 ) ) )
190 173 189 mtbird ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) ∧ 𝑞 ≠ 𝑃 ) → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
191 160 190 pm2.61dane ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) )
192 orel2 ⊢ ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) → ( ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∨ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) → 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
193 191 192 syl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ∨ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( { 𝑞 } ∖ { 𝑃 } ) ) ) ) ) → 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
194 145 193 sylbid ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) → 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) )
195 194 con3d ⊢ ( ( 𝜑 ∧ ( ¬ 𝑞 ∈ 𝑧 ∧ ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 ) ) → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) )
196 195 expr ⊢ ( ( 𝜑 ∧ ¬ 𝑞 ∈ 𝑧 ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ( ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) )
197 196 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑞 ∈ 𝑧 ) → ( ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) )
198 74 197 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑞 ∈ 𝑧 ) → ( ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) )
199 198 expcom ⊢ ( ¬ 𝑞 ∈ 𝑧 → ( 𝜑 → ( ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) ) )
200 199 adantl ⊢ ( ( 𝑧 ∈ Fin ∧ ¬ 𝑞 ∈ 𝑧 ) → ( 𝜑 → ( ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) ) )
201 200 a2d ⊢ ( ( 𝑧 ∈ Fin ∧ ¬ 𝑞 ∈ 𝑧 ) → ( ( 𝜑 → ( 𝑧 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝑧 ∖ { 𝑃 } ) ) ) ) ) ) → ( 𝜑 → ( ( 𝑧 ∪ { 𝑞 } ) ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( ( 𝑧 ∪ { 𝑞 } ) ∖ { 𝑃 } ) ) ) ) ) ) ) )
202 28 37 46 55 70 201 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) ) )
203 14 202 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) ) )
204 15 203 mpi ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ♯ ‘ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ { 𝑃 } ) ) ) ) )