MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfac1eulem Structured version   Visualization version   GIF version

Theorem ablfac1eulem 19858
Description: Lemma for ablfac1eu 19859. (Contributed by Mario Carneiro, 27-Apr-2016.)
Hypotheses
Ref Expression
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
Ref Expression
ablfac1eulem (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))))
Distinct variable groups:   ๐‘ž,๐‘,๐‘ค,๐‘ฅ,๐ต   ๐ท,๐‘,๐‘ž,๐‘ฅ   ๐œ‘,๐‘,๐‘ž,๐‘ค,๐‘ฅ   ๐‘†,๐‘ž   ๐ด,๐‘,๐‘ž,๐‘ฅ   ๐‘‚,๐‘,๐‘ž,๐‘ฅ   ๐‘ƒ,๐‘,๐‘ž,๐‘ฅ   ๐‘‡,๐‘ž,๐‘ฅ   ๐บ,๐‘,๐‘ž,๐‘ฅ
Allowed substitution hints:   ๐ด(๐‘ค)   ๐ถ(๐‘ฅ,๐‘ค,๐‘ž,๐‘)   ๐ท(๐‘ค)   ๐‘ƒ(๐‘ค)   ๐‘†(๐‘ฅ,๐‘ค,๐‘)   ๐‘‡(๐‘ค,๐‘)   ๐บ(๐‘ค)   ๐‘‚(๐‘ค)

Proof of Theorem ablfac1eulem
Dummy variables ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3971 . 2 ๐ด โŠ† ๐ด
2 ablfac1eulem.2 . . 3 (๐œ‘ โ†’ ๐ด โˆˆ Fin)
3 sseq1 3974 . . . . . 6 (๐‘ฆ = โˆ… โ†’ (๐‘ฆ โŠ† ๐ด โ†” โˆ… โŠ† ๐ด))
4 difeq1 4080 . . . . . . . . . . . . 13 (๐‘ฆ = โˆ… โ†’ (๐‘ฆ โˆ– {๐‘ƒ}) = (โˆ… โˆ– {๐‘ƒ}))
5 0dif 4366 . . . . . . . . . . . . 13 (โˆ… โˆ– {๐‘ƒ}) = โˆ…
64, 5eqtrdi 2793 . . . . . . . . . . . 12 (๐‘ฆ = โˆ… โ†’ (๐‘ฆ โˆ– {๐‘ƒ}) = โˆ…)
76reseq2d 5942 . . . . . . . . . . 11 (๐‘ฆ = โˆ… โ†’ (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ โˆ…))
8 res0 5946 . . . . . . . . . . 11 (๐‘‡ โ†พ โˆ…) = โˆ…
97, 8eqtrdi 2793 . . . . . . . . . 10 (๐‘ฆ = โˆ… โ†’ (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})) = โˆ…)
109oveq2d 7378 . . . . . . . . 9 (๐‘ฆ = โˆ… โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))) = (๐บ DProd โˆ…))
1110fveq2d 6851 . . . . . . . 8 (๐‘ฆ = โˆ… โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd โˆ…)))
1211breq2d 5122 . . . . . . 7 (๐‘ฆ = โˆ… โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…))))
1312notbid 318 . . . . . 6 (๐‘ฆ = โˆ… โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…))))
143, 13imbi12d 345 . . . . 5 (๐‘ฆ = โˆ… โ†’ ((๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))))) โ†” (โˆ… โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…)))))
1514imbi2d 341 . . . 4 (๐‘ฆ = โˆ… โ†’ ((๐œ‘ โ†’ (๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))))) โ†” (๐œ‘ โ†’ (โˆ… โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…))))))
16 sseq1 3974 . . . . . 6 (๐‘ฆ = ๐‘ง โ†’ (๐‘ฆ โŠ† ๐ด โ†” ๐‘ง โŠ† ๐ด))
17 difeq1 4080 . . . . . . . . . . 11 (๐‘ฆ = ๐‘ง โ†’ (๐‘ฆ โˆ– {๐‘ƒ}) = (๐‘ง โˆ– {๐‘ƒ}))
1817reseq2d 5942 . . . . . . . . . 10 (๐‘ฆ = ๐‘ง โ†’ (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))
1918oveq2d 7378 . . . . . . . . 9 (๐‘ฆ = ๐‘ง โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))) = (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))
2019fveq2d 6851 . . . . . . . 8 (๐‘ฆ = ๐‘ง โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))))
2120breq2d 5122 . . . . . . 7 (๐‘ฆ = ๐‘ง โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
2221notbid 318 . . . . . 6 (๐‘ฆ = ๐‘ง โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
2316, 22imbi12d 345 . . . . 5 (๐‘ฆ = ๐‘ง โ†’ ((๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))))) โ†” (๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))))))
2423imbi2d 341 . . . 4 (๐‘ฆ = ๐‘ง โ†’ ((๐œ‘ โ†’ (๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))))) โ†” (๐œ‘ โ†’ (๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))))
25 sseq1 3974 . . . . . 6 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (๐‘ฆ โŠ† ๐ด โ†” (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด))
26 difeq1 4080 . . . . . . . . . . 11 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (๐‘ฆ โˆ– {๐‘ƒ}) = ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
2726reseq2d 5942 . . . . . . . . . 10 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))
2827oveq2d 7378 . . . . . . . . 9 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))) = (๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))
2928fveq2d 6851 . . . . . . . 8 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))
3029breq2d 5122 . . . . . . 7 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))
3130notbid 318 . . . . . 6 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))
3225, 31imbi12d 345 . . . . 5 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ ((๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))))) โ†” ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))))
3332imbi2d 341 . . . 4 (๐‘ฆ = (๐‘ง โˆช {๐‘ž}) โ†’ ((๐œ‘ โ†’ (๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))))) โ†” (๐œ‘ โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))))
34 sseq1 3974 . . . . . 6 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ โŠ† ๐ด โ†” ๐ด โŠ† ๐ด))
35 difeq1 4080 . . . . . . . . . . 11 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ โˆ– {๐‘ƒ}) = (๐ด โˆ– {๐‘ƒ}))
3635reseq2d 5942 . . . . . . . . . 10 (๐‘ฆ = ๐ด โ†’ (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))
3736oveq2d 7378 . . . . . . . . 9 (๐‘ฆ = ๐ด โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))) = (๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ}))))
3837fveq2d 6851 . . . . . . . 8 (๐‘ฆ = ๐ด โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))))
3938breq2d 5122 . . . . . . 7 (๐‘ฆ = ๐ด โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ}))))))
4039notbid 318 . . . . . 6 (๐‘ฆ = ๐ด โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))) โ†” ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ}))))))
4134, 40imbi12d 345 . . . . 5 (๐‘ฆ = ๐ด โ†’ ((๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ}))))) โ†” (๐ด โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))))))
4241imbi2d 341 . . . 4 (๐‘ฆ = ๐ด โ†’ ((๐œ‘ โ†’ (๐‘ฆ โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ฆ โˆ– {๐‘ƒ})))))) โ†” (๐œ‘ โ†’ (๐ด โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ}))))))))
43 ablfac1eulem.1 . . . . . . 7 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
44 nprmdvds1 16589 . . . . . . 7 (๐‘ƒ โˆˆ โ„™ โ†’ ยฌ ๐‘ƒ โˆฅ 1)
4543, 44syl 17 . . . . . 6 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ 1)
46 ablfac1.g . . . . . . . . . . 11 (๐œ‘ โ†’ ๐บ โˆˆ Abel)
47 ablgrp 19574 . . . . . . . . . . 11 (๐บ โˆˆ Abel โ†’ ๐บ โˆˆ Grp)
48 eqid 2737 . . . . . . . . . . . 12 (0gโ€˜๐บ) = (0gโ€˜๐บ)
4948dprd0 19817 . . . . . . . . . . 11 (๐บ โˆˆ Grp โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
5046, 47, 493syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บdom DProd โˆ… โˆง (๐บ DProd โˆ…) = {(0gโ€˜๐บ)}))
5150simprd 497 . . . . . . . . 9 (๐œ‘ โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
5251fveq2d 6851 . . . . . . . 8 (๐œ‘ โ†’ (โ™ฏโ€˜(๐บ DProd โˆ…)) = (โ™ฏโ€˜{(0gโ€˜๐บ)}))
53 fvex 6860 . . . . . . . . 9 (0gโ€˜๐บ) โˆˆ V
54 hashsng 14276 . . . . . . . . 9 ((0gโ€˜๐บ) โˆˆ V โ†’ (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1)
5553, 54ax-mp 5 . . . . . . . 8 (โ™ฏโ€˜{(0gโ€˜๐บ)}) = 1
5652, 55eqtrdi 2793 . . . . . . 7 (๐œ‘ โ†’ (โ™ฏโ€˜(๐บ DProd โˆ…)) = 1)
5756breq2d 5122 . . . . . 6 (๐œ‘ โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…)) โ†” ๐‘ƒ โˆฅ 1))
5845, 57mtbird 325 . . . . 5 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…)))
5958a1d 25 . . . 4 (๐œ‘ โ†’ (โˆ… โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd โˆ…))))
60 ssun1 4137 . . . . . . . . . 10 ๐‘ง โŠ† (๐‘ง โˆช {๐‘ž})
61 sstr 3957 . . . . . . . . . 10 ((๐‘ง โŠ† (๐‘ง โˆช {๐‘ž}) โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด) โ†’ ๐‘ง โŠ† ๐ด)
6260, 61mpan 689 . . . . . . . . 9 ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ๐‘ง โŠ† ๐ด)
6362imim1i 63 . . . . . . . 8 ((๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
64 ablfac1eu.1 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐บdom DProd ๐‘‡ โˆง (๐บ DProd ๐‘‡) = ๐ต))
6564simpld 496 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐บdom DProd ๐‘‡)
66 ablfac1eu.2 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ dom ๐‘‡ = ๐ด)
6765, 66dprdf2 19793 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
6867adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐‘‡:๐ดโŸถ(SubGrpโ€˜๐บ))
69 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)
7069ssdifssd 4107 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}) โŠ† ๐ด)
7168, 70fssresd 6714 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})):((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})โŸถ(SubGrpโ€˜๐บ))
72 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ยฌ ๐‘ž โˆˆ ๐‘ง)
73 disjsn 4677 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง โˆฉ {๐‘ž}) = โˆ… โ†” ยฌ ๐‘ž โˆˆ ๐‘ง)
7472, 73sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ง โˆฉ {๐‘ž}) = โˆ…)
7574difeq1d 4086 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘ง โˆฉ {๐‘ž}) โˆ– {๐‘ƒ}) = (โˆ… โˆ– {๐‘ƒ}))
76 difindir 4247 . . . . . . . . . . . . . . . . . 18 ((๐‘ง โˆฉ {๐‘ž}) โˆ– {๐‘ƒ}) = ((๐‘ง โˆ– {๐‘ƒ}) โˆฉ ({๐‘ž} โˆ– {๐‘ƒ}))
7775, 76, 53eqtr3g 2800 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘ง โˆ– {๐‘ƒ}) โˆฉ ({๐‘ž} โˆ– {๐‘ƒ})) = โˆ…)
78 difundir 4245 . . . . . . . . . . . . . . . . . 18 ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}) = ((๐‘ง โˆ– {๐‘ƒ}) โˆช ({๐‘ž} โˆ– {๐‘ƒ}))
7978a1i 11 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}) = ((๐‘ง โˆ– {๐‘ƒ}) โˆช ({๐‘ž} โˆ– {๐‘ƒ})))
80 eqid 2737 . . . . . . . . . . . . . . . . 17 (LSSumโ€˜๐บ) = (LSSumโ€˜๐บ)
8165adantr 482 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐บdom DProd ๐‘‡)
8266adantr 482 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ dom ๐‘‡ = ๐ด)
8381, 82, 70dprdres 19814 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บdom DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โˆง (๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))) โŠ† (๐บ DProd ๐‘‡)))
8483simpld 496 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐บdom DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))
8571, 77, 79, 80, 84dprdsplit 19834 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))) = ((๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
8685fveq2d 6851 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))))
87 eqid 2737 . . . . . . . . . . . . . . . 16 (Cntzโ€˜๐บ) = (Cntzโ€˜๐บ)
8871fdmd 6684 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ dom (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) = ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
89 ssdif 4104 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง โŠ† (๐‘ง โˆช {๐‘ž}) โ†’ (๐‘ง โˆ– {๐‘ƒ}) โŠ† ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
9060, 89mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ง โˆ– {๐‘ƒ}) โŠ† ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
9184, 88, 90dprdres 19814 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})) โˆง (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† (๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))
9291simpld 496 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))
93 dprdsubg 19810 . . . . . . . . . . . . . . . . 17 (๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ (SubGrpโ€˜๐บ))
9492, 93syl 17 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ (SubGrpโ€˜๐บ))
95 ssun2 4138 . . . . . . . . . . . . . . . . . . . 20 {๐‘ž} โŠ† (๐‘ง โˆช {๐‘ž})
96 ssdif 4104 . . . . . . . . . . . . . . . . . . . 20 ({๐‘ž} โŠ† (๐‘ง โˆช {๐‘ž}) โ†’ ({๐‘ž} โˆ– {๐‘ƒ}) โŠ† ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
9795, 96mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ({๐‘ž} โˆ– {๐‘ƒ}) โŠ† ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))
9884, 88, 97dprdres 19814 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})) โˆง (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โŠ† (๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))
9998simpld 496 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))
100 dprdsubg 19810 . . . . . . . . . . . . . . . . 17 (๐บdom DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ (SubGrpโ€˜๐บ))
10199, 100syl 17 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ (SubGrpโ€˜๐บ))
10284, 88, 90, 97, 77, 48dprddisj2 19825 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆฉ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = {(0gโ€˜๐บ)})
10384, 88, 90, 97, 77, 87dprdcntz2 19824 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† ((Cntzโ€˜๐บ)โ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
104 ablfac1.f . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ต โˆˆ Fin)
105104adantr 482 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐ต โˆˆ Fin)
106 ablfac1.b . . . . . . . . . . . . . . . . . 18 ๐ต = (Baseโ€˜๐บ)
107106dprdssv 19802 . . . . . . . . . . . . . . . . 17 (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† ๐ต
108 ssfi 9124 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ Fin)
109105, 107, 108sylancl 587 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ Fin)
110106dprdssv 19802 . . . . . . . . . . . . . . . . 17 (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โŠ† ๐ต
111 ssfi 9124 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โŠ† ๐ต) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ Fin)
112105, 110, 111sylancl 587 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ Fin)
11380, 48, 87, 94, 101, 102, 103, 109, 112lsmhash 19494 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜((๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))(LSSumโ€˜๐บ)(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) = ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))))
11490resabs1d 5973 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))
115114oveq2d 7378 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ}))) = (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))
116115fveq2d 6851 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))))
11797resabs1d 5973 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))
118117oveq2d 7378 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) = (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))
119118fveq2d 6851 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
120116, 119oveq12d 7380 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd ((๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})) โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) = ((โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))))
12186, 113, 1203eqtrd 2781 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))) = ((โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))))
122121breq2d 5122 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ ((โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))))
12343adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐‘ƒ โˆˆ โ„™)
124106dprdssv 19802 . . . . . . . . . . . . . . . . 17 (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† ๐ต
125 ssfi 9124 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โŠ† ๐ต) โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ Fin)
126105, 124, 125sylancl 587 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ Fin)
127 hashcl 14263 . . . . . . . . . . . . . . . 16 ((๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆˆ โ„•0)
128126, 127syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆˆ โ„•0)
129128nn0zd 12532 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆˆ โ„ค)
130106dprdssv 19802 . . . . . . . . . . . . . . . . 17 (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โŠ† ๐ต
131 ssfi 9124 . . . . . . . . . . . . . . . . 17 ((๐ต โˆˆ Fin โˆง (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โŠ† ๐ต) โ†’ (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ Fin)
132105, 130, 131sylancl 587 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ Fin)
133 hashcl 14263 . . . . . . . . . . . . . . . 16 ((๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) โˆˆ Fin โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โˆˆ โ„•0)
134132, 133syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โˆˆ โ„•0)
135134nn0zd 12532 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โˆˆ โ„ค)
136 euclemma 16596 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„™ โˆง (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆˆ โ„ค โˆง (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ ((โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) โ†” (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆจ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))))
137123, 129, 135, 136syl3anc 1372 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ ((โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) ยท (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) โ†” (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆจ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))))
138122, 137bitrd 279 . . . . . . . . . . . 12 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))) โ†” (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆจ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))))
13945ad2antrr 725 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ ยฌ ๐‘ƒ โˆฅ 1)
140 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ ๐‘ž = ๐‘ƒ)
141140sneqd 4603 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ {๐‘ž} = {๐‘ƒ})
142141difeq1d 4086 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ ({๐‘ž} โˆ– {๐‘ƒ}) = ({๐‘ƒ} โˆ– {๐‘ƒ}))
143 difid 4335 . . . . . . . . . . . . . . . . . . . . . . 23 ({๐‘ƒ} โˆ– {๐‘ƒ}) = โˆ…
144142, 143eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ ({๐‘ž} โˆ– {๐‘ƒ}) = โˆ…)
145144reseq2d 5942 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})) = (๐‘‡ โ†พ โˆ…))
146145, 8eqtrdi 2793 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})) = โˆ…)
147146oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) = (๐บ DProd โˆ…))
14851ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐บ DProd โˆ…) = {(0gโ€˜๐บ)})
149147, 148eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) = {(0gโ€˜๐บ)})
150149fveq2d 6851 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜{(0gโ€˜๐บ)}))
151150, 55eqtrdi 2793 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = 1)
152151breq2d 5122 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ 1))
153139, 152mtbird 325 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž = ๐‘ƒ) โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
154 ablfac1.1 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ด โŠ† โ„™)
155154adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐ด โŠ† โ„™)
15669unssbd 4153 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ {๐‘ž} โŠ† ๐ด)
157 vex 3452 . . . . . . . . . . . . . . . . . . . . . 22 ๐‘ž โˆˆ V
158157snss 4751 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ž โˆˆ ๐ด โ†” {๐‘ž} โŠ† ๐ด)
159156, 158sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐‘ž โˆˆ ๐ด)
160155, 159sseldd 3950 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐‘ž โˆˆ โ„™)
161 ablfac1eu.3 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐ถ โˆˆ โ„•0)
162159, 161syldan 592 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ๐ถ โˆˆ โ„•0)
163 prmdvdsexpr 16600 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ž โˆˆ โ„™ โˆง ๐ถ โˆˆ โ„•0) โ†’ (๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ) โ†’ ๐‘ƒ = ๐‘ž))
164123, 160, 162, 163syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ) โ†’ ๐‘ƒ = ๐‘ž))
165 eqcom 2744 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ = ๐‘ž โ†” ๐‘ž = ๐‘ƒ)
166164, 165syl6ib 251 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ) โ†’ ๐‘ž = ๐‘ƒ))
167166necon3ad 2957 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ž โ‰  ๐‘ƒ โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ)))
168167imp 408 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ ยฌ ๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ))
169 disjsn2 4678 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โ‰  ๐‘ƒ โ†’ ({๐‘ž} โˆฉ {๐‘ƒ}) = โˆ…)
170169adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ ({๐‘ž} โˆฉ {๐‘ƒ}) = โˆ…)
171 disj3 4418 . . . . . . . . . . . . . . . . . . . . . 22 (({๐‘ž} โˆฉ {๐‘ƒ}) = โˆ… โ†” {๐‘ž} = ({๐‘ž} โˆ– {๐‘ƒ}))
172170, 171sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ {๐‘ž} = ({๐‘ž} โˆ– {๐‘ƒ}))
173172reseq2d 5942 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (๐‘‡ โ†พ {๐‘ž}) = (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))
174173oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (๐บ DProd (๐‘‡ โ†พ {๐‘ž})) = (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))
17565ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ ๐บdom DProd ๐‘‡)
17666ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ dom ๐‘‡ = ๐ด)
177159adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ ๐‘ž โˆˆ ๐ด)
178175, 176, 177dpjlem 19837 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (๐บ DProd (๐‘‡ โ†พ {๐‘ž})) = (๐‘‡โ€˜๐‘ž))
179174, 178eqtr3d 2779 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))) = (๐‘‡โ€˜๐‘ž))
180179fveq2d 6851 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)))
181 ablfac1eu.4 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘ž โˆˆ ๐ด) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
182159, 181syldan 592 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
183182adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (โ™ฏโ€˜(๐‘‡โ€˜๐‘ž)) = (๐‘žโ†‘๐ถ))
184180, 183eqtrd 2777 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) = (๐‘žโ†‘๐ถ))
185184breq2d 5122 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โ†” ๐‘ƒ โˆฅ (๐‘žโ†‘๐ถ)))
186168, 185mtbird 325 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โˆง ๐‘ž โ‰  ๐‘ƒ) โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
187153, 186pm2.61dane 3033 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))))
188 orel2 890 . . . . . . . . . . . . 13 (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ})))) โ†’ ((๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆจ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) โ†’ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
189187, 188syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ ((๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โˆจ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ({๐‘ž} โˆ– {๐‘ƒ}))))) โ†’ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
190138, 189sylbid 239 . . . . . . . . . . 11 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))) โ†’ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))))
191190con3d 152 . . . . . . . . . 10 ((๐œ‘ โˆง (ยฌ ๐‘ž โˆˆ ๐‘ง โˆง (๐‘ง โˆช {๐‘ž}) โŠ† ๐ด)) โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))
192191expr 458 . . . . . . . . 9 ((๐œ‘ โˆง ยฌ ๐‘ž โˆˆ ๐‘ง) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ (ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))) โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))))
193192a2d 29 . . . . . . . 8 ((๐œ‘ โˆง ยฌ ๐‘ž โˆˆ ๐‘ง) โ†’ (((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))))
19463, 193syl5 34 . . . . . . 7 ((๐œ‘ โˆง ยฌ ๐‘ž โˆˆ ๐‘ง) โ†’ ((๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ})))))))
195194expcom 415 . . . . . 6 (ยฌ ๐‘ž โˆˆ ๐‘ง โ†’ (๐œ‘ โ†’ ((๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))))
196195adantl 483 . . . . 5 ((๐‘ง โˆˆ Fin โˆง ยฌ ๐‘ž โˆˆ ๐‘ง) โ†’ (๐œ‘ โ†’ ((๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ}))))) โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))))
197196a2d 29 . . . 4 ((๐‘ง โˆˆ Fin โˆง ยฌ ๐‘ž โˆˆ ๐‘ง) โ†’ ((๐œ‘ โ†’ (๐‘ง โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐‘ง โˆ– {๐‘ƒ})))))) โ†’ (๐œ‘ โ†’ ((๐‘ง โˆช {๐‘ž}) โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ ((๐‘ง โˆช {๐‘ž}) โˆ– {๐‘ƒ}))))))))
19815, 24, 33, 42, 59, 197findcard2s 9116 . . 3 (๐ด โˆˆ Fin โ†’ (๐œ‘ โ†’ (๐ด โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))))))
1992, 198mpcom 38 . 2 (๐œ‘ โ†’ (๐ด โŠ† ๐ด โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ}))))))
2001, 199mpi 20 1 (๐œ‘ โ†’ ยฌ ๐‘ƒ โˆฅ (โ™ฏโ€˜(๐บ DProd (๐‘‡ โ†พ (๐ด โˆ– {๐‘ƒ})))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  {crab 3410  Vcvv 3448   โˆ– cdif 3912   โˆช cun 3913   โˆฉ cin 3914   โŠ† wss 3915  โˆ…c0 4287  {csn 4591   class class class wbr 5110   โ†ฆ cmpt 5193  dom cdm 5638   โ†พ cres 5640  โŸถwf 6497  โ€˜cfv 6501  (class class class)co 7362  Fincfn 8890  1c1 11059   ยท cmul 11063  โ„•0cn0 12420  โ„คcz 12506  โ†‘cexp 13974  โ™ฏchash 14237   โˆฅ cdvds 16143  โ„™cprime 16554   pCnt cpc 16715  Basecbs 17090  0gc0g 17328  Grpcgrp 18755  SubGrpcsubg 18929  Cntzccntz 19102  odcod 19313  LSSumclsm 19423  Abelcabl 19570   DProd cdprd 19779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-dvds 16144  df-gcd 16382  df-prm 16555  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-0g 17330  df-gsum 17331  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-sbg 18760  df-mulg 18880  df-subg 18932  df-ghm 19013  df-gim 19056  df-cntz 19104  df-oppg 19131  df-lsm 19425  df-pj1 19426  df-cmn 19571  df-abl 19572  df-dprd 19781
This theorem is referenced by:  ablfac1eu  19859
  Copyright terms: Public domain W3C validator